start1(i) -> busy7(F, closed, stop, false, false, false, i)
busy7(BF, d, stop, b1, b2, b3, i) -> incorrect
busy7(FS, d, stop, b1, b2, b3, i) -> incorrect
busy7(fl, open, up, b1, b2, b3, i) -> incorrect
busy7(fl, open, down, b1, b2, b3, i) -> incorrect
busy7(B, closed, stop, false, false, false, empty) -> correct
busy7(F, closed, stop, false, false, false, empty) -> correct
busy7(S, closed, stop, false, false, false, empty) -> correct
busy7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(B, open, stop, false, b2, b3, i) -> idle7(B, closed, stop, false, b2, b3, i)
busy7(F, open, stop, b1, false, b3, i) -> idle7(F, closed, stop, b1, false, b3, i)
busy7(S, open, stop, b1, b2, false, i) -> idle7(S, closed, stop, b1, b2, false, i)
busy7(B, d, stop, true, b2, b3, i) -> idle7(B, open, stop, false, b2, b3, i)
busy7(F, d, stop, b1, true, b3, i) -> idle7(F, open, stop, b1, false, b3, i)
busy7(S, d, stop, b1, b2, true, i) -> idle7(S, open, stop, b1, b2, false, i)
busy7(B, closed, down, b1, b2, b3, i) -> idle7(B, closed, stop, b1, b2, b3, i)
busy7(S, closed, up, b1, b2, b3, i) -> idle7(S, closed, stop, b1, b2, b3, i)
busy7(B, closed, up, true, b2, b3, i) -> idle7(B, closed, stop, true, b2, b3, i)
busy7(F, closed, up, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(F, closed, down, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(S, closed, down, b1, b2, true, i) -> idle7(S, closed, stop, b1, b2, true, i)
busy7(B, closed, up, false, b2, b3, i) -> idle7(BF, closed, up, false, b2, b3, i)
busy7(F, closed, up, b1, false, b3, i) -> idle7(FS, closed, up, b1, false, b3, i)
busy7(F, closed, down, b1, false, b3, i) -> idle7(BF, closed, down, b1, false, b3, i)
busy7(S, closed, down, b1, b2, false, i) -> idle7(FS, closed, down, b1, b2, false, i)
busy7(BF, closed, up, b1, b2, b3, i) -> idle7(F, closed, up, b1, b2, b3, i)
busy7(BF, closed, down, b1, b2, b3, i) -> idle7(B, closed, down, b1, b2, b3, i)
busy7(FS, closed, up, b1, b2, b3, i) -> idle7(S, closed, up, b1, b2, b3, i)
busy7(FS, closed, down, b1, b2, b3, i) -> idle7(F, closed, down, b1, b2, b3, i)
busy7(B, closed, stop, false, true, b3, i) -> idle7(B, closed, up, false, true, b3, i)
busy7(B, closed, stop, false, false, true, i) -> idle7(B, closed, up, false, false, true, i)
busy7(F, closed, stop, true, false, b3, i) -> idle7(F, closed, down, true, false, b3, i)
busy7(F, closed, stop, false, false, true, i) -> idle7(F, closed, up, false, false, true, i)
busy7(S, closed, stop, b1, true, false, i) -> idle7(S, closed, down, b1, true, false, i)
busy7(S, closed, stop, true, false, false, i) -> idle7(S, closed, down, true, false, false, i)
idle7(fl, d, m, b1, b2, b3, empty) -> busy7(fl, d, m, b1, b2, b3, empty)
idle7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> busy7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
or2(true, b) -> true
or2(false, b) -> b
↳ QTRS
↳ Non-Overlap Check
start1(i) -> busy7(F, closed, stop, false, false, false, i)
busy7(BF, d, stop, b1, b2, b3, i) -> incorrect
busy7(FS, d, stop, b1, b2, b3, i) -> incorrect
busy7(fl, open, up, b1, b2, b3, i) -> incorrect
busy7(fl, open, down, b1, b2, b3, i) -> incorrect
busy7(B, closed, stop, false, false, false, empty) -> correct
busy7(F, closed, stop, false, false, false, empty) -> correct
busy7(S, closed, stop, false, false, false, empty) -> correct
busy7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(B, open, stop, false, b2, b3, i) -> idle7(B, closed, stop, false, b2, b3, i)
busy7(F, open, stop, b1, false, b3, i) -> idle7(F, closed, stop, b1, false, b3, i)
busy7(S, open, stop, b1, b2, false, i) -> idle7(S, closed, stop, b1, b2, false, i)
busy7(B, d, stop, true, b2, b3, i) -> idle7(B, open, stop, false, b2, b3, i)
busy7(F, d, stop, b1, true, b3, i) -> idle7(F, open, stop, b1, false, b3, i)
busy7(S, d, stop, b1, b2, true, i) -> idle7(S, open, stop, b1, b2, false, i)
busy7(B, closed, down, b1, b2, b3, i) -> idle7(B, closed, stop, b1, b2, b3, i)
busy7(S, closed, up, b1, b2, b3, i) -> idle7(S, closed, stop, b1, b2, b3, i)
busy7(B, closed, up, true, b2, b3, i) -> idle7(B, closed, stop, true, b2, b3, i)
busy7(F, closed, up, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(F, closed, down, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(S, closed, down, b1, b2, true, i) -> idle7(S, closed, stop, b1, b2, true, i)
busy7(B, closed, up, false, b2, b3, i) -> idle7(BF, closed, up, false, b2, b3, i)
busy7(F, closed, up, b1, false, b3, i) -> idle7(FS, closed, up, b1, false, b3, i)
busy7(F, closed, down, b1, false, b3, i) -> idle7(BF, closed, down, b1, false, b3, i)
busy7(S, closed, down, b1, b2, false, i) -> idle7(FS, closed, down, b1, b2, false, i)
busy7(BF, closed, up, b1, b2, b3, i) -> idle7(F, closed, up, b1, b2, b3, i)
busy7(BF, closed, down, b1, b2, b3, i) -> idle7(B, closed, down, b1, b2, b3, i)
busy7(FS, closed, up, b1, b2, b3, i) -> idle7(S, closed, up, b1, b2, b3, i)
busy7(FS, closed, down, b1, b2, b3, i) -> idle7(F, closed, down, b1, b2, b3, i)
busy7(B, closed, stop, false, true, b3, i) -> idle7(B, closed, up, false, true, b3, i)
busy7(B, closed, stop, false, false, true, i) -> idle7(B, closed, up, false, false, true, i)
busy7(F, closed, stop, true, false, b3, i) -> idle7(F, closed, down, true, false, b3, i)
busy7(F, closed, stop, false, false, true, i) -> idle7(F, closed, up, false, false, true, i)
busy7(S, closed, stop, b1, true, false, i) -> idle7(S, closed, down, b1, true, false, i)
busy7(S, closed, stop, true, false, false, i) -> idle7(S, closed, down, true, false, false, i)
idle7(fl, d, m, b1, b2, b3, empty) -> busy7(fl, d, m, b1, b2, b3, empty)
idle7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> busy7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
or2(true, b) -> true
or2(false, b) -> b
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
start1(i) -> busy7(F, closed, stop, false, false, false, i)
busy7(BF, d, stop, b1, b2, b3, i) -> incorrect
busy7(FS, d, stop, b1, b2, b3, i) -> incorrect
busy7(fl, open, up, b1, b2, b3, i) -> incorrect
busy7(fl, open, down, b1, b2, b3, i) -> incorrect
busy7(B, closed, stop, false, false, false, empty) -> correct
busy7(F, closed, stop, false, false, false, empty) -> correct
busy7(S, closed, stop, false, false, false, empty) -> correct
busy7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(B, open, stop, false, b2, b3, i) -> idle7(B, closed, stop, false, b2, b3, i)
busy7(F, open, stop, b1, false, b3, i) -> idle7(F, closed, stop, b1, false, b3, i)
busy7(S, open, stop, b1, b2, false, i) -> idle7(S, closed, stop, b1, b2, false, i)
busy7(B, d, stop, true, b2, b3, i) -> idle7(B, open, stop, false, b2, b3, i)
busy7(F, d, stop, b1, true, b3, i) -> idle7(F, open, stop, b1, false, b3, i)
busy7(S, d, stop, b1, b2, true, i) -> idle7(S, open, stop, b1, b2, false, i)
busy7(B, closed, down, b1, b2, b3, i) -> idle7(B, closed, stop, b1, b2, b3, i)
busy7(S, closed, up, b1, b2, b3, i) -> idle7(S, closed, stop, b1, b2, b3, i)
busy7(B, closed, up, true, b2, b3, i) -> idle7(B, closed, stop, true, b2, b3, i)
busy7(F, closed, up, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(F, closed, down, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(S, closed, down, b1, b2, true, i) -> idle7(S, closed, stop, b1, b2, true, i)
busy7(B, closed, up, false, b2, b3, i) -> idle7(BF, closed, up, false, b2, b3, i)
busy7(F, closed, up, b1, false, b3, i) -> idle7(FS, closed, up, b1, false, b3, i)
busy7(F, closed, down, b1, false, b3, i) -> idle7(BF, closed, down, b1, false, b3, i)
busy7(S, closed, down, b1, b2, false, i) -> idle7(FS, closed, down, b1, b2, false, i)
busy7(BF, closed, up, b1, b2, b3, i) -> idle7(F, closed, up, b1, b2, b3, i)
busy7(BF, closed, down, b1, b2, b3, i) -> idle7(B, closed, down, b1, b2, b3, i)
busy7(FS, closed, up, b1, b2, b3, i) -> idle7(S, closed, up, b1, b2, b3, i)
busy7(FS, closed, down, b1, b2, b3, i) -> idle7(F, closed, down, b1, b2, b3, i)
busy7(B, closed, stop, false, true, b3, i) -> idle7(B, closed, up, false, true, b3, i)
busy7(B, closed, stop, false, false, true, i) -> idle7(B, closed, up, false, false, true, i)
busy7(F, closed, stop, true, false, b3, i) -> idle7(F, closed, down, true, false, b3, i)
busy7(F, closed, stop, false, false, true, i) -> idle7(F, closed, up, false, false, true, i)
busy7(S, closed, stop, b1, true, false, i) -> idle7(S, closed, down, b1, true, false, i)
busy7(S, closed, stop, true, false, false, i) -> idle7(S, closed, down, true, false, false, i)
idle7(fl, d, m, b1, b2, b3, empty) -> busy7(fl, d, m, b1, b2, b3, empty)
idle7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> busy7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
or2(true, b) -> true
or2(false, b) -> b
start1(x0)
busy7(BF, x0, stop, x1, x2, x3, x4)
busy7(FS, x0, stop, x1, x2, x3, x4)
busy7(x0, open, up, x1, x2, x3, x4)
busy7(x0, open, down, x1, x2, x3, x4)
busy7(B, closed, stop, false, false, false, empty)
busy7(F, closed, stop, false, false, false, empty)
busy7(S, closed, stop, false, false, false, empty)
busy7(B, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(F, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(S, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(B, open, stop, false, x0, x1, x2)
busy7(F, open, stop, x0, false, x1, x2)
busy7(S, open, stop, x0, x1, false, x2)
busy7(B, x0, stop, true, x1, x2, x3)
busy7(F, x0, stop, x1, true, x2, x3)
busy7(S, x0, stop, x1, x2, true, x3)
busy7(B, closed, down, x0, x1, x2, x3)
busy7(S, closed, up, x0, x1, x2, x3)
busy7(B, closed, up, true, x0, x1, x2)
busy7(F, closed, up, x0, true, x1, x2)
busy7(F, closed, down, x0, true, x1, x2)
busy7(S, closed, down, x0, x1, true, x2)
busy7(B, closed, up, false, x0, x1, x2)
busy7(F, closed, up, x0, false, x1, x2)
busy7(F, closed, down, x0, false, x1, x2)
busy7(S, closed, down, x0, x1, false, x2)
busy7(BF, closed, up, x0, x1, x2, x3)
busy7(BF, closed, down, x0, x1, x2, x3)
busy7(FS, closed, up, x0, x1, x2, x3)
busy7(FS, closed, down, x0, x1, x2, x3)
busy7(B, closed, stop, false, true, x0, x1)
busy7(B, closed, stop, false, false, true, x0)
busy7(F, closed, stop, true, false, x0, x1)
busy7(F, closed, stop, false, false, true, x0)
busy7(S, closed, stop, x0, true, false, x1)
busy7(S, closed, stop, true, false, false, x0)
idle7(x0, x1, x2, x3, x4, x5, empty)
idle7(x0, x1, x2, x3, x4, x5, newbuttons4(x6, x7, x8, x9))
or2(true, x0)
or2(false, x0)
BUSY7(S, closed, stop, true, false, false, i) -> IDLE7(S, closed, down, true, false, false, i)
IDLE7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> BUSY7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
BUSY7(B, open, stop, false, b2, b3, i) -> IDLE7(B, closed, stop, false, b2, b3, i)
BUSY7(S, d, stop, b1, b2, true, i) -> IDLE7(S, open, stop, b1, b2, false, i)
BUSY7(F, open, stop, b1, false, b3, i) -> IDLE7(F, closed, stop, b1, false, b3, i)
BUSY7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
BUSY7(F, closed, stop, true, false, b3, i) -> IDLE7(F, closed, down, true, false, b3, i)
BUSY7(B, closed, stop, false, true, b3, i) -> IDLE7(B, closed, up, false, true, b3, i)
BUSY7(F, closed, stop, false, false, true, i) -> IDLE7(F, closed, up, false, false, true, i)
BUSY7(S, open, stop, b1, b2, false, i) -> IDLE7(S, closed, stop, b1, b2, false, i)
BUSY7(BF, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, down, b1, b2, b3, i)
IDLE7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> OR2(b3, i3)
START1(i) -> BUSY7(F, closed, stop, false, false, false, i)
IDLE7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> OR2(b2, i2)
BUSY7(BF, closed, up, b1, b2, b3, i) -> IDLE7(F, closed, up, b1, b2, b3, i)
BUSY7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
BUSY7(F, d, stop, b1, true, b3, i) -> IDLE7(F, open, stop, b1, false, b3, i)
BUSY7(B, closed, stop, false, false, true, i) -> IDLE7(B, closed, up, false, false, true, i)
BUSY7(F, closed, down, b1, false, b3, i) -> IDLE7(BF, closed, down, b1, false, b3, i)
BUSY7(FS, closed, down, b1, b2, b3, i) -> IDLE7(F, closed, down, b1, b2, b3, i)
BUSY7(S, closed, stop, b1, true, false, i) -> IDLE7(S, closed, down, b1, true, false, i)
BUSY7(F, closed, up, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(S, closed, down, b1, b2, true, i) -> IDLE7(S, closed, stop, b1, b2, true, i)
BUSY7(F, closed, up, b1, false, b3, i) -> IDLE7(FS, closed, up, b1, false, b3, i)
BUSY7(F, closed, down, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
IDLE7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> OR2(b1, i1)
IDLE7(fl, d, m, b1, b2, b3, empty) -> BUSY7(fl, d, m, b1, b2, b3, empty)
BUSY7(S, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, stop, b1, b2, b3, i)
BUSY7(B, closed, up, false, b2, b3, i) -> IDLE7(BF, closed, up, false, b2, b3, i)
BUSY7(B, d, stop, true, b2, b3, i) -> IDLE7(B, open, stop, false, b2, b3, i)
BUSY7(S, closed, down, b1, b2, false, i) -> IDLE7(FS, closed, down, b1, b2, false, i)
BUSY7(B, closed, up, true, b2, b3, i) -> IDLE7(B, closed, stop, true, b2, b3, i)
BUSY7(B, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, stop, b1, b2, b3, i)
BUSY7(FS, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, up, b1, b2, b3, i)
start1(i) -> busy7(F, closed, stop, false, false, false, i)
busy7(BF, d, stop, b1, b2, b3, i) -> incorrect
busy7(FS, d, stop, b1, b2, b3, i) -> incorrect
busy7(fl, open, up, b1, b2, b3, i) -> incorrect
busy7(fl, open, down, b1, b2, b3, i) -> incorrect
busy7(B, closed, stop, false, false, false, empty) -> correct
busy7(F, closed, stop, false, false, false, empty) -> correct
busy7(S, closed, stop, false, false, false, empty) -> correct
busy7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(B, open, stop, false, b2, b3, i) -> idle7(B, closed, stop, false, b2, b3, i)
busy7(F, open, stop, b1, false, b3, i) -> idle7(F, closed, stop, b1, false, b3, i)
busy7(S, open, stop, b1, b2, false, i) -> idle7(S, closed, stop, b1, b2, false, i)
busy7(B, d, stop, true, b2, b3, i) -> idle7(B, open, stop, false, b2, b3, i)
busy7(F, d, stop, b1, true, b3, i) -> idle7(F, open, stop, b1, false, b3, i)
busy7(S, d, stop, b1, b2, true, i) -> idle7(S, open, stop, b1, b2, false, i)
busy7(B, closed, down, b1, b2, b3, i) -> idle7(B, closed, stop, b1, b2, b3, i)
busy7(S, closed, up, b1, b2, b3, i) -> idle7(S, closed, stop, b1, b2, b3, i)
busy7(B, closed, up, true, b2, b3, i) -> idle7(B, closed, stop, true, b2, b3, i)
busy7(F, closed, up, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(F, closed, down, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(S, closed, down, b1, b2, true, i) -> idle7(S, closed, stop, b1, b2, true, i)
busy7(B, closed, up, false, b2, b3, i) -> idle7(BF, closed, up, false, b2, b3, i)
busy7(F, closed, up, b1, false, b3, i) -> idle7(FS, closed, up, b1, false, b3, i)
busy7(F, closed, down, b1, false, b3, i) -> idle7(BF, closed, down, b1, false, b3, i)
busy7(S, closed, down, b1, b2, false, i) -> idle7(FS, closed, down, b1, b2, false, i)
busy7(BF, closed, up, b1, b2, b3, i) -> idle7(F, closed, up, b1, b2, b3, i)
busy7(BF, closed, down, b1, b2, b3, i) -> idle7(B, closed, down, b1, b2, b3, i)
busy7(FS, closed, up, b1, b2, b3, i) -> idle7(S, closed, up, b1, b2, b3, i)
busy7(FS, closed, down, b1, b2, b3, i) -> idle7(F, closed, down, b1, b2, b3, i)
busy7(B, closed, stop, false, true, b3, i) -> idle7(B, closed, up, false, true, b3, i)
busy7(B, closed, stop, false, false, true, i) -> idle7(B, closed, up, false, false, true, i)
busy7(F, closed, stop, true, false, b3, i) -> idle7(F, closed, down, true, false, b3, i)
busy7(F, closed, stop, false, false, true, i) -> idle7(F, closed, up, false, false, true, i)
busy7(S, closed, stop, b1, true, false, i) -> idle7(S, closed, down, b1, true, false, i)
busy7(S, closed, stop, true, false, false, i) -> idle7(S, closed, down, true, false, false, i)
idle7(fl, d, m, b1, b2, b3, empty) -> busy7(fl, d, m, b1, b2, b3, empty)
idle7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> busy7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
or2(true, b) -> true
or2(false, b) -> b
start1(x0)
busy7(BF, x0, stop, x1, x2, x3, x4)
busy7(FS, x0, stop, x1, x2, x3, x4)
busy7(x0, open, up, x1, x2, x3, x4)
busy7(x0, open, down, x1, x2, x3, x4)
busy7(B, closed, stop, false, false, false, empty)
busy7(F, closed, stop, false, false, false, empty)
busy7(S, closed, stop, false, false, false, empty)
busy7(B, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(F, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(S, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(B, open, stop, false, x0, x1, x2)
busy7(F, open, stop, x0, false, x1, x2)
busy7(S, open, stop, x0, x1, false, x2)
busy7(B, x0, stop, true, x1, x2, x3)
busy7(F, x0, stop, x1, true, x2, x3)
busy7(S, x0, stop, x1, x2, true, x3)
busy7(B, closed, down, x0, x1, x2, x3)
busy7(S, closed, up, x0, x1, x2, x3)
busy7(B, closed, up, true, x0, x1, x2)
busy7(F, closed, up, x0, true, x1, x2)
busy7(F, closed, down, x0, true, x1, x2)
busy7(S, closed, down, x0, x1, true, x2)
busy7(B, closed, up, false, x0, x1, x2)
busy7(F, closed, up, x0, false, x1, x2)
busy7(F, closed, down, x0, false, x1, x2)
busy7(S, closed, down, x0, x1, false, x2)
busy7(BF, closed, up, x0, x1, x2, x3)
busy7(BF, closed, down, x0, x1, x2, x3)
busy7(FS, closed, up, x0, x1, x2, x3)
busy7(FS, closed, down, x0, x1, x2, x3)
busy7(B, closed, stop, false, true, x0, x1)
busy7(B, closed, stop, false, false, true, x0)
busy7(F, closed, stop, true, false, x0, x1)
busy7(F, closed, stop, false, false, true, x0)
busy7(S, closed, stop, x0, true, false, x1)
busy7(S, closed, stop, true, false, false, x0)
idle7(x0, x1, x2, x3, x4, x5, empty)
idle7(x0, x1, x2, x3, x4, x5, newbuttons4(x6, x7, x8, x9))
or2(true, x0)
or2(false, x0)
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
BUSY7(S, closed, stop, true, false, false, i) -> IDLE7(S, closed, down, true, false, false, i)
IDLE7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> BUSY7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
BUSY7(B, open, stop, false, b2, b3, i) -> IDLE7(B, closed, stop, false, b2, b3, i)
BUSY7(S, d, stop, b1, b2, true, i) -> IDLE7(S, open, stop, b1, b2, false, i)
BUSY7(F, open, stop, b1, false, b3, i) -> IDLE7(F, closed, stop, b1, false, b3, i)
BUSY7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
BUSY7(F, closed, stop, true, false, b3, i) -> IDLE7(F, closed, down, true, false, b3, i)
BUSY7(B, closed, stop, false, true, b3, i) -> IDLE7(B, closed, up, false, true, b3, i)
BUSY7(F, closed, stop, false, false, true, i) -> IDLE7(F, closed, up, false, false, true, i)
BUSY7(S, open, stop, b1, b2, false, i) -> IDLE7(S, closed, stop, b1, b2, false, i)
BUSY7(BF, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, down, b1, b2, b3, i)
IDLE7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> OR2(b3, i3)
START1(i) -> BUSY7(F, closed, stop, false, false, false, i)
IDLE7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> OR2(b2, i2)
BUSY7(BF, closed, up, b1, b2, b3, i) -> IDLE7(F, closed, up, b1, b2, b3, i)
BUSY7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
BUSY7(F, d, stop, b1, true, b3, i) -> IDLE7(F, open, stop, b1, false, b3, i)
BUSY7(B, closed, stop, false, false, true, i) -> IDLE7(B, closed, up, false, false, true, i)
BUSY7(F, closed, down, b1, false, b3, i) -> IDLE7(BF, closed, down, b1, false, b3, i)
BUSY7(FS, closed, down, b1, b2, b3, i) -> IDLE7(F, closed, down, b1, b2, b3, i)
BUSY7(S, closed, stop, b1, true, false, i) -> IDLE7(S, closed, down, b1, true, false, i)
BUSY7(F, closed, up, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(S, closed, down, b1, b2, true, i) -> IDLE7(S, closed, stop, b1, b2, true, i)
BUSY7(F, closed, up, b1, false, b3, i) -> IDLE7(FS, closed, up, b1, false, b3, i)
BUSY7(F, closed, down, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
IDLE7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> OR2(b1, i1)
IDLE7(fl, d, m, b1, b2, b3, empty) -> BUSY7(fl, d, m, b1, b2, b3, empty)
BUSY7(S, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, stop, b1, b2, b3, i)
BUSY7(B, closed, up, false, b2, b3, i) -> IDLE7(BF, closed, up, false, b2, b3, i)
BUSY7(B, d, stop, true, b2, b3, i) -> IDLE7(B, open, stop, false, b2, b3, i)
BUSY7(S, closed, down, b1, b2, false, i) -> IDLE7(FS, closed, down, b1, b2, false, i)
BUSY7(B, closed, up, true, b2, b3, i) -> IDLE7(B, closed, stop, true, b2, b3, i)
BUSY7(B, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, stop, b1, b2, b3, i)
BUSY7(FS, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, up, b1, b2, b3, i)
start1(i) -> busy7(F, closed, stop, false, false, false, i)
busy7(BF, d, stop, b1, b2, b3, i) -> incorrect
busy7(FS, d, stop, b1, b2, b3, i) -> incorrect
busy7(fl, open, up, b1, b2, b3, i) -> incorrect
busy7(fl, open, down, b1, b2, b3, i) -> incorrect
busy7(B, closed, stop, false, false, false, empty) -> correct
busy7(F, closed, stop, false, false, false, empty) -> correct
busy7(S, closed, stop, false, false, false, empty) -> correct
busy7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(B, open, stop, false, b2, b3, i) -> idle7(B, closed, stop, false, b2, b3, i)
busy7(F, open, stop, b1, false, b3, i) -> idle7(F, closed, stop, b1, false, b3, i)
busy7(S, open, stop, b1, b2, false, i) -> idle7(S, closed, stop, b1, b2, false, i)
busy7(B, d, stop, true, b2, b3, i) -> idle7(B, open, stop, false, b2, b3, i)
busy7(F, d, stop, b1, true, b3, i) -> idle7(F, open, stop, b1, false, b3, i)
busy7(S, d, stop, b1, b2, true, i) -> idle7(S, open, stop, b1, b2, false, i)
busy7(B, closed, down, b1, b2, b3, i) -> idle7(B, closed, stop, b1, b2, b3, i)
busy7(S, closed, up, b1, b2, b3, i) -> idle7(S, closed, stop, b1, b2, b3, i)
busy7(B, closed, up, true, b2, b3, i) -> idle7(B, closed, stop, true, b2, b3, i)
busy7(F, closed, up, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(F, closed, down, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(S, closed, down, b1, b2, true, i) -> idle7(S, closed, stop, b1, b2, true, i)
busy7(B, closed, up, false, b2, b3, i) -> idle7(BF, closed, up, false, b2, b3, i)
busy7(F, closed, up, b1, false, b3, i) -> idle7(FS, closed, up, b1, false, b3, i)
busy7(F, closed, down, b1, false, b3, i) -> idle7(BF, closed, down, b1, false, b3, i)
busy7(S, closed, down, b1, b2, false, i) -> idle7(FS, closed, down, b1, b2, false, i)
busy7(BF, closed, up, b1, b2, b3, i) -> idle7(F, closed, up, b1, b2, b3, i)
busy7(BF, closed, down, b1, b2, b3, i) -> idle7(B, closed, down, b1, b2, b3, i)
busy7(FS, closed, up, b1, b2, b3, i) -> idle7(S, closed, up, b1, b2, b3, i)
busy7(FS, closed, down, b1, b2, b3, i) -> idle7(F, closed, down, b1, b2, b3, i)
busy7(B, closed, stop, false, true, b3, i) -> idle7(B, closed, up, false, true, b3, i)
busy7(B, closed, stop, false, false, true, i) -> idle7(B, closed, up, false, false, true, i)
busy7(F, closed, stop, true, false, b3, i) -> idle7(F, closed, down, true, false, b3, i)
busy7(F, closed, stop, false, false, true, i) -> idle7(F, closed, up, false, false, true, i)
busy7(S, closed, stop, b1, true, false, i) -> idle7(S, closed, down, b1, true, false, i)
busy7(S, closed, stop, true, false, false, i) -> idle7(S, closed, down, true, false, false, i)
idle7(fl, d, m, b1, b2, b3, empty) -> busy7(fl, d, m, b1, b2, b3, empty)
idle7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> busy7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
or2(true, b) -> true
or2(false, b) -> b
start1(x0)
busy7(BF, x0, stop, x1, x2, x3, x4)
busy7(FS, x0, stop, x1, x2, x3, x4)
busy7(x0, open, up, x1, x2, x3, x4)
busy7(x0, open, down, x1, x2, x3, x4)
busy7(B, closed, stop, false, false, false, empty)
busy7(F, closed, stop, false, false, false, empty)
busy7(S, closed, stop, false, false, false, empty)
busy7(B, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(F, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(S, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(B, open, stop, false, x0, x1, x2)
busy7(F, open, stop, x0, false, x1, x2)
busy7(S, open, stop, x0, x1, false, x2)
busy7(B, x0, stop, true, x1, x2, x3)
busy7(F, x0, stop, x1, true, x2, x3)
busy7(S, x0, stop, x1, x2, true, x3)
busy7(B, closed, down, x0, x1, x2, x3)
busy7(S, closed, up, x0, x1, x2, x3)
busy7(B, closed, up, true, x0, x1, x2)
busy7(F, closed, up, x0, true, x1, x2)
busy7(F, closed, down, x0, true, x1, x2)
busy7(S, closed, down, x0, x1, true, x2)
busy7(B, closed, up, false, x0, x1, x2)
busy7(F, closed, up, x0, false, x1, x2)
busy7(F, closed, down, x0, false, x1, x2)
busy7(S, closed, down, x0, x1, false, x2)
busy7(BF, closed, up, x0, x1, x2, x3)
busy7(BF, closed, down, x0, x1, x2, x3)
busy7(FS, closed, up, x0, x1, x2, x3)
busy7(FS, closed, down, x0, x1, x2, x3)
busy7(B, closed, stop, false, true, x0, x1)
busy7(B, closed, stop, false, false, true, x0)
busy7(F, closed, stop, true, false, x0, x1)
busy7(F, closed, stop, false, false, true, x0)
busy7(S, closed, stop, x0, true, false, x1)
busy7(S, closed, stop, true, false, false, x0)
idle7(x0, x1, x2, x3, x4, x5, empty)
idle7(x0, x1, x2, x3, x4, x5, newbuttons4(x6, x7, x8, x9))
or2(true, x0)
or2(false, x0)
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
BUSY7(S, closed, stop, true, false, false, i) -> IDLE7(S, closed, down, true, false, false, i)
IDLE7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> BUSY7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
BUSY7(B, open, stop, false, b2, b3, i) -> IDLE7(B, closed, stop, false, b2, b3, i)
BUSY7(S, d, stop, b1, b2, true, i) -> IDLE7(S, open, stop, b1, b2, false, i)
BUSY7(F, open, stop, b1, false, b3, i) -> IDLE7(F, closed, stop, b1, false, b3, i)
BUSY7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
BUSY7(F, closed, stop, true, false, b3, i) -> IDLE7(F, closed, down, true, false, b3, i)
BUSY7(B, closed, stop, false, true, b3, i) -> IDLE7(B, closed, up, false, true, b3, i)
BUSY7(F, closed, stop, false, false, true, i) -> IDLE7(F, closed, up, false, false, true, i)
BUSY7(S, open, stop, b1, b2, false, i) -> IDLE7(S, closed, stop, b1, b2, false, i)
BUSY7(BF, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, down, b1, b2, b3, i)
BUSY7(BF, closed, up, b1, b2, b3, i) -> IDLE7(F, closed, up, b1, b2, b3, i)
BUSY7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
BUSY7(F, d, stop, b1, true, b3, i) -> IDLE7(F, open, stop, b1, false, b3, i)
BUSY7(B, closed, stop, false, false, true, i) -> IDLE7(B, closed, up, false, false, true, i)
BUSY7(F, closed, down, b1, false, b3, i) -> IDLE7(BF, closed, down, b1, false, b3, i)
BUSY7(FS, closed, down, b1, b2, b3, i) -> IDLE7(F, closed, down, b1, b2, b3, i)
BUSY7(S, closed, stop, b1, true, false, i) -> IDLE7(S, closed, down, b1, true, false, i)
BUSY7(F, closed, up, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(S, closed, down, b1, b2, true, i) -> IDLE7(S, closed, stop, b1, b2, true, i)
BUSY7(F, closed, up, b1, false, b3, i) -> IDLE7(FS, closed, up, b1, false, b3, i)
BUSY7(F, closed, down, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
IDLE7(fl, d, m, b1, b2, b3, empty) -> BUSY7(fl, d, m, b1, b2, b3, empty)
BUSY7(S, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, stop, b1, b2, b3, i)
BUSY7(B, closed, up, false, b2, b3, i) -> IDLE7(BF, closed, up, false, b2, b3, i)
BUSY7(B, d, stop, true, b2, b3, i) -> IDLE7(B, open, stop, false, b2, b3, i)
BUSY7(S, closed, down, b1, b2, false, i) -> IDLE7(FS, closed, down, b1, b2, false, i)
BUSY7(B, closed, up, true, b2, b3, i) -> IDLE7(B, closed, stop, true, b2, b3, i)
BUSY7(B, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, stop, b1, b2, b3, i)
BUSY7(FS, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, up, b1, b2, b3, i)
start1(i) -> busy7(F, closed, stop, false, false, false, i)
busy7(BF, d, stop, b1, b2, b3, i) -> incorrect
busy7(FS, d, stop, b1, b2, b3, i) -> incorrect
busy7(fl, open, up, b1, b2, b3, i) -> incorrect
busy7(fl, open, down, b1, b2, b3, i) -> incorrect
busy7(B, closed, stop, false, false, false, empty) -> correct
busy7(F, closed, stop, false, false, false, empty) -> correct
busy7(S, closed, stop, false, false, false, empty) -> correct
busy7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(B, open, stop, false, b2, b3, i) -> idle7(B, closed, stop, false, b2, b3, i)
busy7(F, open, stop, b1, false, b3, i) -> idle7(F, closed, stop, b1, false, b3, i)
busy7(S, open, stop, b1, b2, false, i) -> idle7(S, closed, stop, b1, b2, false, i)
busy7(B, d, stop, true, b2, b3, i) -> idle7(B, open, stop, false, b2, b3, i)
busy7(F, d, stop, b1, true, b3, i) -> idle7(F, open, stop, b1, false, b3, i)
busy7(S, d, stop, b1, b2, true, i) -> idle7(S, open, stop, b1, b2, false, i)
busy7(B, closed, down, b1, b2, b3, i) -> idle7(B, closed, stop, b1, b2, b3, i)
busy7(S, closed, up, b1, b2, b3, i) -> idle7(S, closed, stop, b1, b2, b3, i)
busy7(B, closed, up, true, b2, b3, i) -> idle7(B, closed, stop, true, b2, b3, i)
busy7(F, closed, up, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(F, closed, down, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(S, closed, down, b1, b2, true, i) -> idle7(S, closed, stop, b1, b2, true, i)
busy7(B, closed, up, false, b2, b3, i) -> idle7(BF, closed, up, false, b2, b3, i)
busy7(F, closed, up, b1, false, b3, i) -> idle7(FS, closed, up, b1, false, b3, i)
busy7(F, closed, down, b1, false, b3, i) -> idle7(BF, closed, down, b1, false, b3, i)
busy7(S, closed, down, b1, b2, false, i) -> idle7(FS, closed, down, b1, b2, false, i)
busy7(BF, closed, up, b1, b2, b3, i) -> idle7(F, closed, up, b1, b2, b3, i)
busy7(BF, closed, down, b1, b2, b3, i) -> idle7(B, closed, down, b1, b2, b3, i)
busy7(FS, closed, up, b1, b2, b3, i) -> idle7(S, closed, up, b1, b2, b3, i)
busy7(FS, closed, down, b1, b2, b3, i) -> idle7(F, closed, down, b1, b2, b3, i)
busy7(B, closed, stop, false, true, b3, i) -> idle7(B, closed, up, false, true, b3, i)
busy7(B, closed, stop, false, false, true, i) -> idle7(B, closed, up, false, false, true, i)
busy7(F, closed, stop, true, false, b3, i) -> idle7(F, closed, down, true, false, b3, i)
busy7(F, closed, stop, false, false, true, i) -> idle7(F, closed, up, false, false, true, i)
busy7(S, closed, stop, b1, true, false, i) -> idle7(S, closed, down, b1, true, false, i)
busy7(S, closed, stop, true, false, false, i) -> idle7(S, closed, down, true, false, false, i)
idle7(fl, d, m, b1, b2, b3, empty) -> busy7(fl, d, m, b1, b2, b3, empty)
idle7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> busy7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
or2(true, b) -> true
or2(false, b) -> b
start1(x0)
busy7(BF, x0, stop, x1, x2, x3, x4)
busy7(FS, x0, stop, x1, x2, x3, x4)
busy7(x0, open, up, x1, x2, x3, x4)
busy7(x0, open, down, x1, x2, x3, x4)
busy7(B, closed, stop, false, false, false, empty)
busy7(F, closed, stop, false, false, false, empty)
busy7(S, closed, stop, false, false, false, empty)
busy7(B, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(F, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(S, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(B, open, stop, false, x0, x1, x2)
busy7(F, open, stop, x0, false, x1, x2)
busy7(S, open, stop, x0, x1, false, x2)
busy7(B, x0, stop, true, x1, x2, x3)
busy7(F, x0, stop, x1, true, x2, x3)
busy7(S, x0, stop, x1, x2, true, x3)
busy7(B, closed, down, x0, x1, x2, x3)
busy7(S, closed, up, x0, x1, x2, x3)
busy7(B, closed, up, true, x0, x1, x2)
busy7(F, closed, up, x0, true, x1, x2)
busy7(F, closed, down, x0, true, x1, x2)
busy7(S, closed, down, x0, x1, true, x2)
busy7(B, closed, up, false, x0, x1, x2)
busy7(F, closed, up, x0, false, x1, x2)
busy7(F, closed, down, x0, false, x1, x2)
busy7(S, closed, down, x0, x1, false, x2)
busy7(BF, closed, up, x0, x1, x2, x3)
busy7(BF, closed, down, x0, x1, x2, x3)
busy7(FS, closed, up, x0, x1, x2, x3)
busy7(FS, closed, down, x0, x1, x2, x3)
busy7(B, closed, stop, false, true, x0, x1)
busy7(B, closed, stop, false, false, true, x0)
busy7(F, closed, stop, true, false, x0, x1)
busy7(F, closed, stop, false, false, true, x0)
busy7(S, closed, stop, x0, true, false, x1)
busy7(S, closed, stop, true, false, false, x0)
idle7(x0, x1, x2, x3, x4, x5, empty)
idle7(x0, x1, x2, x3, x4, x5, newbuttons4(x6, x7, x8, x9))
or2(true, x0)
or2(false, x0)
The following pairs can be strictly oriented and are deleted.
The remaining pairs can at least by weakly be oriented.
IDLE7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> BUSY7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
Used ordering: Combined order from the following AFS and order.
BUSY7(S, closed, stop, true, false, false, i) -> IDLE7(S, closed, down, true, false, false, i)
BUSY7(B, open, stop, false, b2, b3, i) -> IDLE7(B, closed, stop, false, b2, b3, i)
BUSY7(S, d, stop, b1, b2, true, i) -> IDLE7(S, open, stop, b1, b2, false, i)
BUSY7(F, open, stop, b1, false, b3, i) -> IDLE7(F, closed, stop, b1, false, b3, i)
BUSY7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
BUSY7(F, closed, stop, true, false, b3, i) -> IDLE7(F, closed, down, true, false, b3, i)
BUSY7(B, closed, stop, false, true, b3, i) -> IDLE7(B, closed, up, false, true, b3, i)
BUSY7(F, closed, stop, false, false, true, i) -> IDLE7(F, closed, up, false, false, true, i)
BUSY7(S, open, stop, b1, b2, false, i) -> IDLE7(S, closed, stop, b1, b2, false, i)
BUSY7(BF, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, down, b1, b2, b3, i)
BUSY7(BF, closed, up, b1, b2, b3, i) -> IDLE7(F, closed, up, b1, b2, b3, i)
BUSY7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
BUSY7(F, d, stop, b1, true, b3, i) -> IDLE7(F, open, stop, b1, false, b3, i)
BUSY7(B, closed, stop, false, false, true, i) -> IDLE7(B, closed, up, false, false, true, i)
BUSY7(F, closed, down, b1, false, b3, i) -> IDLE7(BF, closed, down, b1, false, b3, i)
BUSY7(FS, closed, down, b1, b2, b3, i) -> IDLE7(F, closed, down, b1, b2, b3, i)
BUSY7(S, closed, stop, b1, true, false, i) -> IDLE7(S, closed, down, b1, true, false, i)
BUSY7(F, closed, up, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(S, closed, down, b1, b2, true, i) -> IDLE7(S, closed, stop, b1, b2, true, i)
BUSY7(F, closed, up, b1, false, b3, i) -> IDLE7(FS, closed, up, b1, false, b3, i)
BUSY7(F, closed, down, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
IDLE7(fl, d, m, b1, b2, b3, empty) -> BUSY7(fl, d, m, b1, b2, b3, empty)
BUSY7(S, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, stop, b1, b2, b3, i)
BUSY7(B, closed, up, false, b2, b3, i) -> IDLE7(BF, closed, up, false, b2, b3, i)
BUSY7(B, d, stop, true, b2, b3, i) -> IDLE7(B, open, stop, false, b2, b3, i)
BUSY7(S, closed, down, b1, b2, false, i) -> IDLE7(FS, closed, down, b1, b2, false, i)
BUSY7(B, closed, up, true, b2, b3, i) -> IDLE7(B, closed, stop, true, b2, b3, i)
BUSY7(B, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, stop, b1, b2, b3, i)
BUSY7(FS, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, up, b1, b2, b3, i)
down > S > newbuttons1 > or2 > true > closed > B > open
down > S > newbuttons1 > or2 > true > stop > B > open
down > S > newbuttons1 > or2 > true > false > B > open
down > S > newbuttons1 > or2 > true > up > B > open
down > S > FS > closed > B > open
down > S > FS > up > B > open
down > BF > F > newbuttons1 > or2 > true > closed > B > open
down > BF > F > newbuttons1 > or2 > true > stop > B > open
down > BF > F > newbuttons1 > or2 > true > false > B > open
down > BF > F > newbuttons1 > or2 > true > up > B > open
empty > open
or2(true, b) -> true
or2(false, b) -> b
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
BUSY7(S, closed, stop, true, false, false, i) -> IDLE7(S, closed, down, true, false, false, i)
BUSY7(B, open, stop, false, b2, b3, i) -> IDLE7(B, closed, stop, false, b2, b3, i)
BUSY7(S, d, stop, b1, b2, true, i) -> IDLE7(S, open, stop, b1, b2, false, i)
BUSY7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
BUSY7(F, open, stop, b1, false, b3, i) -> IDLE7(F, closed, stop, b1, false, b3, i)
BUSY7(B, closed, stop, false, true, b3, i) -> IDLE7(B, closed, up, false, true, b3, i)
BUSY7(F, closed, stop, true, false, b3, i) -> IDLE7(F, closed, down, true, false, b3, i)
BUSY7(F, closed, stop, false, false, true, i) -> IDLE7(F, closed, up, false, false, true, i)
BUSY7(BF, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, down, b1, b2, b3, i)
BUSY7(S, open, stop, b1, b2, false, i) -> IDLE7(S, closed, stop, b1, b2, false, i)
BUSY7(BF, closed, up, b1, b2, b3, i) -> IDLE7(F, closed, up, b1, b2, b3, i)
BUSY7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
BUSY7(F, d, stop, b1, true, b3, i) -> IDLE7(F, open, stop, b1, false, b3, i)
BUSY7(B, closed, stop, false, false, true, i) -> IDLE7(B, closed, up, false, false, true, i)
BUSY7(F, closed, down, b1, false, b3, i) -> IDLE7(BF, closed, down, b1, false, b3, i)
BUSY7(FS, closed, down, b1, b2, b3, i) -> IDLE7(F, closed, down, b1, b2, b3, i)
BUSY7(S, closed, stop, b1, true, false, i) -> IDLE7(S, closed, down, b1, true, false, i)
BUSY7(F, closed, up, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(S, closed, down, b1, b2, true, i) -> IDLE7(S, closed, stop, b1, b2, true, i)
BUSY7(F, closed, up, b1, false, b3, i) -> IDLE7(FS, closed, up, b1, false, b3, i)
BUSY7(F, closed, down, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> IDLE7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
IDLE7(fl, d, m, b1, b2, b3, empty) -> BUSY7(fl, d, m, b1, b2, b3, empty)
BUSY7(S, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, stop, b1, b2, b3, i)
BUSY7(B, closed, up, false, b2, b3, i) -> IDLE7(BF, closed, up, false, b2, b3, i)
BUSY7(B, d, stop, true, b2, b3, i) -> IDLE7(B, open, stop, false, b2, b3, i)
BUSY7(S, closed, down, b1, b2, false, i) -> IDLE7(FS, closed, down, b1, b2, false, i)
BUSY7(B, closed, up, true, b2, b3, i) -> IDLE7(B, closed, stop, true, b2, b3, i)
BUSY7(FS, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, up, b1, b2, b3, i)
BUSY7(B, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, stop, b1, b2, b3, i)
start1(i) -> busy7(F, closed, stop, false, false, false, i)
busy7(BF, d, stop, b1, b2, b3, i) -> incorrect
busy7(FS, d, stop, b1, b2, b3, i) -> incorrect
busy7(fl, open, up, b1, b2, b3, i) -> incorrect
busy7(fl, open, down, b1, b2, b3, i) -> incorrect
busy7(B, closed, stop, false, false, false, empty) -> correct
busy7(F, closed, stop, false, false, false, empty) -> correct
busy7(S, closed, stop, false, false, false, empty) -> correct
busy7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(B, open, stop, false, b2, b3, i) -> idle7(B, closed, stop, false, b2, b3, i)
busy7(F, open, stop, b1, false, b3, i) -> idle7(F, closed, stop, b1, false, b3, i)
busy7(S, open, stop, b1, b2, false, i) -> idle7(S, closed, stop, b1, b2, false, i)
busy7(B, d, stop, true, b2, b3, i) -> idle7(B, open, stop, false, b2, b3, i)
busy7(F, d, stop, b1, true, b3, i) -> idle7(F, open, stop, b1, false, b3, i)
busy7(S, d, stop, b1, b2, true, i) -> idle7(S, open, stop, b1, b2, false, i)
busy7(B, closed, down, b1, b2, b3, i) -> idle7(B, closed, stop, b1, b2, b3, i)
busy7(S, closed, up, b1, b2, b3, i) -> idle7(S, closed, stop, b1, b2, b3, i)
busy7(B, closed, up, true, b2, b3, i) -> idle7(B, closed, stop, true, b2, b3, i)
busy7(F, closed, up, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(F, closed, down, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(S, closed, down, b1, b2, true, i) -> idle7(S, closed, stop, b1, b2, true, i)
busy7(B, closed, up, false, b2, b3, i) -> idle7(BF, closed, up, false, b2, b3, i)
busy7(F, closed, up, b1, false, b3, i) -> idle7(FS, closed, up, b1, false, b3, i)
busy7(F, closed, down, b1, false, b3, i) -> idle7(BF, closed, down, b1, false, b3, i)
busy7(S, closed, down, b1, b2, false, i) -> idle7(FS, closed, down, b1, b2, false, i)
busy7(BF, closed, up, b1, b2, b3, i) -> idle7(F, closed, up, b1, b2, b3, i)
busy7(BF, closed, down, b1, b2, b3, i) -> idle7(B, closed, down, b1, b2, b3, i)
busy7(FS, closed, up, b1, b2, b3, i) -> idle7(S, closed, up, b1, b2, b3, i)
busy7(FS, closed, down, b1, b2, b3, i) -> idle7(F, closed, down, b1, b2, b3, i)
busy7(B, closed, stop, false, true, b3, i) -> idle7(B, closed, up, false, true, b3, i)
busy7(B, closed, stop, false, false, true, i) -> idle7(B, closed, up, false, false, true, i)
busy7(F, closed, stop, true, false, b3, i) -> idle7(F, closed, down, true, false, b3, i)
busy7(F, closed, stop, false, false, true, i) -> idle7(F, closed, up, false, false, true, i)
busy7(S, closed, stop, b1, true, false, i) -> idle7(S, closed, down, b1, true, false, i)
busy7(S, closed, stop, true, false, false, i) -> idle7(S, closed, down, true, false, false, i)
idle7(fl, d, m, b1, b2, b3, empty) -> busy7(fl, d, m, b1, b2, b3, empty)
idle7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> busy7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
or2(true, b) -> true
or2(false, b) -> b
start1(x0)
busy7(BF, x0, stop, x1, x2, x3, x4)
busy7(FS, x0, stop, x1, x2, x3, x4)
busy7(x0, open, up, x1, x2, x3, x4)
busy7(x0, open, down, x1, x2, x3, x4)
busy7(B, closed, stop, false, false, false, empty)
busy7(F, closed, stop, false, false, false, empty)
busy7(S, closed, stop, false, false, false, empty)
busy7(B, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(F, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(S, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(B, open, stop, false, x0, x1, x2)
busy7(F, open, stop, x0, false, x1, x2)
busy7(S, open, stop, x0, x1, false, x2)
busy7(B, x0, stop, true, x1, x2, x3)
busy7(F, x0, stop, x1, true, x2, x3)
busy7(S, x0, stop, x1, x2, true, x3)
busy7(B, closed, down, x0, x1, x2, x3)
busy7(S, closed, up, x0, x1, x2, x3)
busy7(B, closed, up, true, x0, x1, x2)
busy7(F, closed, up, x0, true, x1, x2)
busy7(F, closed, down, x0, true, x1, x2)
busy7(S, closed, down, x0, x1, true, x2)
busy7(B, closed, up, false, x0, x1, x2)
busy7(F, closed, up, x0, false, x1, x2)
busy7(F, closed, down, x0, false, x1, x2)
busy7(S, closed, down, x0, x1, false, x2)
busy7(BF, closed, up, x0, x1, x2, x3)
busy7(BF, closed, down, x0, x1, x2, x3)
busy7(FS, closed, up, x0, x1, x2, x3)
busy7(FS, closed, down, x0, x1, x2, x3)
busy7(B, closed, stop, false, true, x0, x1)
busy7(B, closed, stop, false, false, true, x0)
busy7(F, closed, stop, true, false, x0, x1)
busy7(F, closed, stop, false, false, true, x0)
busy7(S, closed, stop, x0, true, false, x1)
busy7(S, closed, stop, true, false, false, x0)
idle7(x0, x1, x2, x3, x4, x5, empty)
idle7(x0, x1, x2, x3, x4, x5, newbuttons4(x6, x7, x8, x9))
or2(true, x0)
or2(false, x0)
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
BUSY7(S, closed, stop, true, false, false, i) -> IDLE7(S, closed, down, true, false, false, i)
BUSY7(B, open, stop, false, b2, b3, i) -> IDLE7(B, closed, stop, false, b2, b3, i)
BUSY7(S, d, stop, b1, b2, true, i) -> IDLE7(S, open, stop, b1, b2, false, i)
BUSY7(F, open, stop, b1, false, b3, i) -> IDLE7(F, closed, stop, b1, false, b3, i)
BUSY7(B, closed, stop, false, true, b3, i) -> IDLE7(B, closed, up, false, true, b3, i)
BUSY7(F, closed, stop, true, false, b3, i) -> IDLE7(F, closed, down, true, false, b3, i)
BUSY7(F, closed, stop, false, false, true, i) -> IDLE7(F, closed, up, false, false, true, i)
BUSY7(S, open, stop, b1, b2, false, i) -> IDLE7(S, closed, stop, b1, b2, false, i)
BUSY7(BF, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, down, b1, b2, b3, i)
BUSY7(BF, closed, up, b1, b2, b3, i) -> IDLE7(F, closed, up, b1, b2, b3, i)
BUSY7(F, d, stop, b1, true, b3, i) -> IDLE7(F, open, stop, b1, false, b3, i)
BUSY7(F, closed, down, b1, false, b3, i) -> IDLE7(BF, closed, down, b1, false, b3, i)
BUSY7(FS, closed, down, b1, b2, b3, i) -> IDLE7(F, closed, down, b1, b2, b3, i)
BUSY7(B, closed, stop, false, false, true, i) -> IDLE7(B, closed, up, false, false, true, i)
BUSY7(S, closed, stop, b1, true, false, i) -> IDLE7(S, closed, down, b1, true, false, i)
BUSY7(S, closed, down, b1, b2, true, i) -> IDLE7(S, closed, stop, b1, b2, true, i)
BUSY7(F, closed, up, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(F, closed, up, b1, false, b3, i) -> IDLE7(FS, closed, up, b1, false, b3, i)
BUSY7(F, closed, down, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
IDLE7(fl, d, m, b1, b2, b3, empty) -> BUSY7(fl, d, m, b1, b2, b3, empty)
BUSY7(S, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, stop, b1, b2, b3, i)
BUSY7(B, closed, up, false, b2, b3, i) -> IDLE7(BF, closed, up, false, b2, b3, i)
BUSY7(B, d, stop, true, b2, b3, i) -> IDLE7(B, open, stop, false, b2, b3, i)
BUSY7(S, closed, down, b1, b2, false, i) -> IDLE7(FS, closed, down, b1, b2, false, i)
BUSY7(B, closed, up, true, b2, b3, i) -> IDLE7(B, closed, stop, true, b2, b3, i)
BUSY7(B, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, stop, b1, b2, b3, i)
BUSY7(FS, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, up, b1, b2, b3, i)
start1(i) -> busy7(F, closed, stop, false, false, false, i)
busy7(BF, d, stop, b1, b2, b3, i) -> incorrect
busy7(FS, d, stop, b1, b2, b3, i) -> incorrect
busy7(fl, open, up, b1, b2, b3, i) -> incorrect
busy7(fl, open, down, b1, b2, b3, i) -> incorrect
busy7(B, closed, stop, false, false, false, empty) -> correct
busy7(F, closed, stop, false, false, false, empty) -> correct
busy7(S, closed, stop, false, false, false, empty) -> correct
busy7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(B, open, stop, false, b2, b3, i) -> idle7(B, closed, stop, false, b2, b3, i)
busy7(F, open, stop, b1, false, b3, i) -> idle7(F, closed, stop, b1, false, b3, i)
busy7(S, open, stop, b1, b2, false, i) -> idle7(S, closed, stop, b1, b2, false, i)
busy7(B, d, stop, true, b2, b3, i) -> idle7(B, open, stop, false, b2, b3, i)
busy7(F, d, stop, b1, true, b3, i) -> idle7(F, open, stop, b1, false, b3, i)
busy7(S, d, stop, b1, b2, true, i) -> idle7(S, open, stop, b1, b2, false, i)
busy7(B, closed, down, b1, b2, b3, i) -> idle7(B, closed, stop, b1, b2, b3, i)
busy7(S, closed, up, b1, b2, b3, i) -> idle7(S, closed, stop, b1, b2, b3, i)
busy7(B, closed, up, true, b2, b3, i) -> idle7(B, closed, stop, true, b2, b3, i)
busy7(F, closed, up, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(F, closed, down, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(S, closed, down, b1, b2, true, i) -> idle7(S, closed, stop, b1, b2, true, i)
busy7(B, closed, up, false, b2, b3, i) -> idle7(BF, closed, up, false, b2, b3, i)
busy7(F, closed, up, b1, false, b3, i) -> idle7(FS, closed, up, b1, false, b3, i)
busy7(F, closed, down, b1, false, b3, i) -> idle7(BF, closed, down, b1, false, b3, i)
busy7(S, closed, down, b1, b2, false, i) -> idle7(FS, closed, down, b1, b2, false, i)
busy7(BF, closed, up, b1, b2, b3, i) -> idle7(F, closed, up, b1, b2, b3, i)
busy7(BF, closed, down, b1, b2, b3, i) -> idle7(B, closed, down, b1, b2, b3, i)
busy7(FS, closed, up, b1, b2, b3, i) -> idle7(S, closed, up, b1, b2, b3, i)
busy7(FS, closed, down, b1, b2, b3, i) -> idle7(F, closed, down, b1, b2, b3, i)
busy7(B, closed, stop, false, true, b3, i) -> idle7(B, closed, up, false, true, b3, i)
busy7(B, closed, stop, false, false, true, i) -> idle7(B, closed, up, false, false, true, i)
busy7(F, closed, stop, true, false, b3, i) -> idle7(F, closed, down, true, false, b3, i)
busy7(F, closed, stop, false, false, true, i) -> idle7(F, closed, up, false, false, true, i)
busy7(S, closed, stop, b1, true, false, i) -> idle7(S, closed, down, b1, true, false, i)
busy7(S, closed, stop, true, false, false, i) -> idle7(S, closed, down, true, false, false, i)
idle7(fl, d, m, b1, b2, b3, empty) -> busy7(fl, d, m, b1, b2, b3, empty)
idle7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> busy7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
or2(true, b) -> true
or2(false, b) -> b
start1(x0)
busy7(BF, x0, stop, x1, x2, x3, x4)
busy7(FS, x0, stop, x1, x2, x3, x4)
busy7(x0, open, up, x1, x2, x3, x4)
busy7(x0, open, down, x1, x2, x3, x4)
busy7(B, closed, stop, false, false, false, empty)
busy7(F, closed, stop, false, false, false, empty)
busy7(S, closed, stop, false, false, false, empty)
busy7(B, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(F, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(S, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(B, open, stop, false, x0, x1, x2)
busy7(F, open, stop, x0, false, x1, x2)
busy7(S, open, stop, x0, x1, false, x2)
busy7(B, x0, stop, true, x1, x2, x3)
busy7(F, x0, stop, x1, true, x2, x3)
busy7(S, x0, stop, x1, x2, true, x3)
busy7(B, closed, down, x0, x1, x2, x3)
busy7(S, closed, up, x0, x1, x2, x3)
busy7(B, closed, up, true, x0, x1, x2)
busy7(F, closed, up, x0, true, x1, x2)
busy7(F, closed, down, x0, true, x1, x2)
busy7(S, closed, down, x0, x1, true, x2)
busy7(B, closed, up, false, x0, x1, x2)
busy7(F, closed, up, x0, false, x1, x2)
busy7(F, closed, down, x0, false, x1, x2)
busy7(S, closed, down, x0, x1, false, x2)
busy7(BF, closed, up, x0, x1, x2, x3)
busy7(BF, closed, down, x0, x1, x2, x3)
busy7(FS, closed, up, x0, x1, x2, x3)
busy7(FS, closed, down, x0, x1, x2, x3)
busy7(B, closed, stop, false, true, x0, x1)
busy7(B, closed, stop, false, false, true, x0)
busy7(F, closed, stop, true, false, x0, x1)
busy7(F, closed, stop, false, false, true, x0)
busy7(S, closed, stop, x0, true, false, x1)
busy7(S, closed, stop, true, false, false, x0)
idle7(x0, x1, x2, x3, x4, x5, empty)
idle7(x0, x1, x2, x3, x4, x5, newbuttons4(x6, x7, x8, x9))
or2(true, x0)
or2(false, x0)
The following pairs can be strictly oriented and are deleted.
The remaining pairs can at least by weakly be oriented.
BUSY7(B, d, stop, true, b2, b3, i) -> IDLE7(B, open, stop, false, b2, b3, i)
Used ordering: Combined order from the following AFS and order.
BUSY7(S, closed, stop, true, false, false, i) -> IDLE7(S, closed, down, true, false, false, i)
BUSY7(B, open, stop, false, b2, b3, i) -> IDLE7(B, closed, stop, false, b2, b3, i)
BUSY7(S, d, stop, b1, b2, true, i) -> IDLE7(S, open, stop, b1, b2, false, i)
BUSY7(F, open, stop, b1, false, b3, i) -> IDLE7(F, closed, stop, b1, false, b3, i)
BUSY7(B, closed, stop, false, true, b3, i) -> IDLE7(B, closed, up, false, true, b3, i)
BUSY7(F, closed, stop, true, false, b3, i) -> IDLE7(F, closed, down, true, false, b3, i)
BUSY7(F, closed, stop, false, false, true, i) -> IDLE7(F, closed, up, false, false, true, i)
BUSY7(S, open, stop, b1, b2, false, i) -> IDLE7(S, closed, stop, b1, b2, false, i)
BUSY7(BF, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, down, b1, b2, b3, i)
BUSY7(BF, closed, up, b1, b2, b3, i) -> IDLE7(F, closed, up, b1, b2, b3, i)
BUSY7(F, d, stop, b1, true, b3, i) -> IDLE7(F, open, stop, b1, false, b3, i)
BUSY7(F, closed, down, b1, false, b3, i) -> IDLE7(BF, closed, down, b1, false, b3, i)
BUSY7(FS, closed, down, b1, b2, b3, i) -> IDLE7(F, closed, down, b1, b2, b3, i)
BUSY7(B, closed, stop, false, false, true, i) -> IDLE7(B, closed, up, false, false, true, i)
BUSY7(S, closed, stop, b1, true, false, i) -> IDLE7(S, closed, down, b1, true, false, i)
BUSY7(S, closed, down, b1, b2, true, i) -> IDLE7(S, closed, stop, b1, b2, true, i)
BUSY7(F, closed, up, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(F, closed, up, b1, false, b3, i) -> IDLE7(FS, closed, up, b1, false, b3, i)
BUSY7(F, closed, down, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
IDLE7(fl, d, m, b1, b2, b3, empty) -> BUSY7(fl, d, m, b1, b2, b3, empty)
BUSY7(S, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, stop, b1, b2, b3, i)
BUSY7(B, closed, up, false, b2, b3, i) -> IDLE7(BF, closed, up, false, b2, b3, i)
BUSY7(S, closed, down, b1, b2, false, i) -> IDLE7(FS, closed, down, b1, b2, false, i)
BUSY7(B, closed, up, true, b2, b3, i) -> IDLE7(B, closed, stop, true, b2, b3, i)
BUSY7(B, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, stop, b1, b2, b3, i)
BUSY7(FS, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, up, b1, b2, b3, i)
up > true > S > closed > stop > B > BF > open
up > true > S > closed > down > B > BF > open
up > true > S > closed > down > FS > open
up > true > S > false > stop > B > BF > open
up > true > S > false > down > B > BF > open
up > true > S > false > down > FS > open
up > true > F > stop > B > BF > open
up > true > F > down > B > BF > open
up > true > F > down > FS > open
empty > open
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
BUSY7(S, closed, stop, true, false, false, i) -> IDLE7(S, closed, down, true, false, false, i)
BUSY7(B, open, stop, false, b2, b3, i) -> IDLE7(B, closed, stop, false, b2, b3, i)
BUSY7(S, d, stop, b1, b2, true, i) -> IDLE7(S, open, stop, b1, b2, false, i)
BUSY7(F, open, stop, b1, false, b3, i) -> IDLE7(F, closed, stop, b1, false, b3, i)
BUSY7(F, closed, stop, true, false, b3, i) -> IDLE7(F, closed, down, true, false, b3, i)
BUSY7(B, closed, stop, false, true, b3, i) -> IDLE7(B, closed, up, false, true, b3, i)
BUSY7(F, closed, stop, false, false, true, i) -> IDLE7(F, closed, up, false, false, true, i)
BUSY7(BF, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, down, b1, b2, b3, i)
BUSY7(S, open, stop, b1, b2, false, i) -> IDLE7(S, closed, stop, b1, b2, false, i)
BUSY7(BF, closed, up, b1, b2, b3, i) -> IDLE7(F, closed, up, b1, b2, b3, i)
BUSY7(F, d, stop, b1, true, b3, i) -> IDLE7(F, open, stop, b1, false, b3, i)
BUSY7(FS, closed, down, b1, b2, b3, i) -> IDLE7(F, closed, down, b1, b2, b3, i)
BUSY7(F, closed, down, b1, false, b3, i) -> IDLE7(BF, closed, down, b1, false, b3, i)
BUSY7(B, closed, stop, false, false, true, i) -> IDLE7(B, closed, up, false, false, true, i)
BUSY7(S, closed, stop, b1, true, false, i) -> IDLE7(S, closed, down, b1, true, false, i)
BUSY7(S, closed, down, b1, b2, true, i) -> IDLE7(S, closed, stop, b1, b2, true, i)
BUSY7(F, closed, up, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(F, closed, up, b1, false, b3, i) -> IDLE7(FS, closed, up, b1, false, b3, i)
BUSY7(F, closed, down, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
IDLE7(fl, d, m, b1, b2, b3, empty) -> BUSY7(fl, d, m, b1, b2, b3, empty)
BUSY7(S, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, stop, b1, b2, b3, i)
BUSY7(B, closed, up, false, b2, b3, i) -> IDLE7(BF, closed, up, false, b2, b3, i)
BUSY7(S, closed, down, b1, b2, false, i) -> IDLE7(FS, closed, down, b1, b2, false, i)
BUSY7(B, closed, up, true, b2, b3, i) -> IDLE7(B, closed, stop, true, b2, b3, i)
BUSY7(FS, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, up, b1, b2, b3, i)
BUSY7(B, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, stop, b1, b2, b3, i)
start1(i) -> busy7(F, closed, stop, false, false, false, i)
busy7(BF, d, stop, b1, b2, b3, i) -> incorrect
busy7(FS, d, stop, b1, b2, b3, i) -> incorrect
busy7(fl, open, up, b1, b2, b3, i) -> incorrect
busy7(fl, open, down, b1, b2, b3, i) -> incorrect
busy7(B, closed, stop, false, false, false, empty) -> correct
busy7(F, closed, stop, false, false, false, empty) -> correct
busy7(S, closed, stop, false, false, false, empty) -> correct
busy7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(B, open, stop, false, b2, b3, i) -> idle7(B, closed, stop, false, b2, b3, i)
busy7(F, open, stop, b1, false, b3, i) -> idle7(F, closed, stop, b1, false, b3, i)
busy7(S, open, stop, b1, b2, false, i) -> idle7(S, closed, stop, b1, b2, false, i)
busy7(B, d, stop, true, b2, b3, i) -> idle7(B, open, stop, false, b2, b3, i)
busy7(F, d, stop, b1, true, b3, i) -> idle7(F, open, stop, b1, false, b3, i)
busy7(S, d, stop, b1, b2, true, i) -> idle7(S, open, stop, b1, b2, false, i)
busy7(B, closed, down, b1, b2, b3, i) -> idle7(B, closed, stop, b1, b2, b3, i)
busy7(S, closed, up, b1, b2, b3, i) -> idle7(S, closed, stop, b1, b2, b3, i)
busy7(B, closed, up, true, b2, b3, i) -> idle7(B, closed, stop, true, b2, b3, i)
busy7(F, closed, up, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(F, closed, down, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(S, closed, down, b1, b2, true, i) -> idle7(S, closed, stop, b1, b2, true, i)
busy7(B, closed, up, false, b2, b3, i) -> idle7(BF, closed, up, false, b2, b3, i)
busy7(F, closed, up, b1, false, b3, i) -> idle7(FS, closed, up, b1, false, b3, i)
busy7(F, closed, down, b1, false, b3, i) -> idle7(BF, closed, down, b1, false, b3, i)
busy7(S, closed, down, b1, b2, false, i) -> idle7(FS, closed, down, b1, b2, false, i)
busy7(BF, closed, up, b1, b2, b3, i) -> idle7(F, closed, up, b1, b2, b3, i)
busy7(BF, closed, down, b1, b2, b3, i) -> idle7(B, closed, down, b1, b2, b3, i)
busy7(FS, closed, up, b1, b2, b3, i) -> idle7(S, closed, up, b1, b2, b3, i)
busy7(FS, closed, down, b1, b2, b3, i) -> idle7(F, closed, down, b1, b2, b3, i)
busy7(B, closed, stop, false, true, b3, i) -> idle7(B, closed, up, false, true, b3, i)
busy7(B, closed, stop, false, false, true, i) -> idle7(B, closed, up, false, false, true, i)
busy7(F, closed, stop, true, false, b3, i) -> idle7(F, closed, down, true, false, b3, i)
busy7(F, closed, stop, false, false, true, i) -> idle7(F, closed, up, false, false, true, i)
busy7(S, closed, stop, b1, true, false, i) -> idle7(S, closed, down, b1, true, false, i)
busy7(S, closed, stop, true, false, false, i) -> idle7(S, closed, down, true, false, false, i)
idle7(fl, d, m, b1, b2, b3, empty) -> busy7(fl, d, m, b1, b2, b3, empty)
idle7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> busy7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
or2(true, b) -> true
or2(false, b) -> b
start1(x0)
busy7(BF, x0, stop, x1, x2, x3, x4)
busy7(FS, x0, stop, x1, x2, x3, x4)
busy7(x0, open, up, x1, x2, x3, x4)
busy7(x0, open, down, x1, x2, x3, x4)
busy7(B, closed, stop, false, false, false, empty)
busy7(F, closed, stop, false, false, false, empty)
busy7(S, closed, stop, false, false, false, empty)
busy7(B, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(F, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(S, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(B, open, stop, false, x0, x1, x2)
busy7(F, open, stop, x0, false, x1, x2)
busy7(S, open, stop, x0, x1, false, x2)
busy7(B, x0, stop, true, x1, x2, x3)
busy7(F, x0, stop, x1, true, x2, x3)
busy7(S, x0, stop, x1, x2, true, x3)
busy7(B, closed, down, x0, x1, x2, x3)
busy7(S, closed, up, x0, x1, x2, x3)
busy7(B, closed, up, true, x0, x1, x2)
busy7(F, closed, up, x0, true, x1, x2)
busy7(F, closed, down, x0, true, x1, x2)
busy7(S, closed, down, x0, x1, true, x2)
busy7(B, closed, up, false, x0, x1, x2)
busy7(F, closed, up, x0, false, x1, x2)
busy7(F, closed, down, x0, false, x1, x2)
busy7(S, closed, down, x0, x1, false, x2)
busy7(BF, closed, up, x0, x1, x2, x3)
busy7(BF, closed, down, x0, x1, x2, x3)
busy7(FS, closed, up, x0, x1, x2, x3)
busy7(FS, closed, down, x0, x1, x2, x3)
busy7(B, closed, stop, false, true, x0, x1)
busy7(B, closed, stop, false, false, true, x0)
busy7(F, closed, stop, true, false, x0, x1)
busy7(F, closed, stop, false, false, true, x0)
busy7(S, closed, stop, x0, true, false, x1)
busy7(S, closed, stop, true, false, false, x0)
idle7(x0, x1, x2, x3, x4, x5, empty)
idle7(x0, x1, x2, x3, x4, x5, newbuttons4(x6, x7, x8, x9))
or2(true, x0)
or2(false, x0)
The following pairs can be strictly oriented and are deleted.
The remaining pairs can at least by weakly be oriented.
BUSY7(S, d, stop, b1, b2, true, i) -> IDLE7(S, open, stop, b1, b2, false, i)
Used ordering: Combined order from the following AFS and order.
BUSY7(S, closed, stop, true, false, false, i) -> IDLE7(S, closed, down, true, false, false, i)
BUSY7(B, open, stop, false, b2, b3, i) -> IDLE7(B, closed, stop, false, b2, b3, i)
BUSY7(F, open, stop, b1, false, b3, i) -> IDLE7(F, closed, stop, b1, false, b3, i)
BUSY7(F, closed, stop, true, false, b3, i) -> IDLE7(F, closed, down, true, false, b3, i)
BUSY7(B, closed, stop, false, true, b3, i) -> IDLE7(B, closed, up, false, true, b3, i)
BUSY7(F, closed, stop, false, false, true, i) -> IDLE7(F, closed, up, false, false, true, i)
BUSY7(BF, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, down, b1, b2, b3, i)
BUSY7(S, open, stop, b1, b2, false, i) -> IDLE7(S, closed, stop, b1, b2, false, i)
BUSY7(BF, closed, up, b1, b2, b3, i) -> IDLE7(F, closed, up, b1, b2, b3, i)
BUSY7(F, d, stop, b1, true, b3, i) -> IDLE7(F, open, stop, b1, false, b3, i)
BUSY7(FS, closed, down, b1, b2, b3, i) -> IDLE7(F, closed, down, b1, b2, b3, i)
BUSY7(F, closed, down, b1, false, b3, i) -> IDLE7(BF, closed, down, b1, false, b3, i)
BUSY7(B, closed, stop, false, false, true, i) -> IDLE7(B, closed, up, false, false, true, i)
BUSY7(S, closed, stop, b1, true, false, i) -> IDLE7(S, closed, down, b1, true, false, i)
BUSY7(S, closed, down, b1, b2, true, i) -> IDLE7(S, closed, stop, b1, b2, true, i)
BUSY7(F, closed, up, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(F, closed, up, b1, false, b3, i) -> IDLE7(FS, closed, up, b1, false, b3, i)
BUSY7(F, closed, down, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
IDLE7(fl, d, m, b1, b2, b3, empty) -> BUSY7(fl, d, m, b1, b2, b3, empty)
BUSY7(S, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, stop, b1, b2, b3, i)
BUSY7(B, closed, up, false, b2, b3, i) -> IDLE7(BF, closed, up, false, b2, b3, i)
BUSY7(S, closed, down, b1, b2, false, i) -> IDLE7(FS, closed, down, b1, b2, false, i)
BUSY7(B, closed, up, true, b2, b3, i) -> IDLE7(B, closed, stop, true, b2, b3, i)
BUSY7(FS, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, up, b1, b2, b3, i)
BUSY7(B, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, stop, b1, b2, b3, i)
closed > stop > true > B > false > S > down > open
closed > stop > F > BF > B > false > S > down > open
closed > FS > up > true > B > false > S > down > open
closed > FS > up > F > BF > B > false > S > down > open
empty > open
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
BUSY7(S, closed, stop, true, false, false, i) -> IDLE7(S, closed, down, true, false, false, i)
BUSY7(B, open, stop, false, b2, b3, i) -> IDLE7(B, closed, stop, false, b2, b3, i)
BUSY7(F, open, stop, b1, false, b3, i) -> IDLE7(F, closed, stop, b1, false, b3, i)
BUSY7(B, closed, stop, false, true, b3, i) -> IDLE7(B, closed, up, false, true, b3, i)
BUSY7(F, closed, stop, true, false, b3, i) -> IDLE7(F, closed, down, true, false, b3, i)
BUSY7(F, closed, stop, false, false, true, i) -> IDLE7(F, closed, up, false, false, true, i)
BUSY7(S, open, stop, b1, b2, false, i) -> IDLE7(S, closed, stop, b1, b2, false, i)
BUSY7(BF, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, down, b1, b2, b3, i)
BUSY7(BF, closed, up, b1, b2, b3, i) -> IDLE7(F, closed, up, b1, b2, b3, i)
BUSY7(F, d, stop, b1, true, b3, i) -> IDLE7(F, open, stop, b1, false, b3, i)
BUSY7(B, closed, stop, false, false, true, i) -> IDLE7(B, closed, up, false, false, true, i)
BUSY7(F, closed, down, b1, false, b3, i) -> IDLE7(BF, closed, down, b1, false, b3, i)
BUSY7(FS, closed, down, b1, b2, b3, i) -> IDLE7(F, closed, down, b1, b2, b3, i)
BUSY7(S, closed, stop, b1, true, false, i) -> IDLE7(S, closed, down, b1, true, false, i)
BUSY7(S, closed, down, b1, b2, true, i) -> IDLE7(S, closed, stop, b1, b2, true, i)
BUSY7(F, closed, up, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(F, closed, up, b1, false, b3, i) -> IDLE7(FS, closed, up, b1, false, b3, i)
BUSY7(F, closed, down, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
IDLE7(fl, d, m, b1, b2, b3, empty) -> BUSY7(fl, d, m, b1, b2, b3, empty)
BUSY7(S, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, stop, b1, b2, b3, i)
BUSY7(B, closed, up, false, b2, b3, i) -> IDLE7(BF, closed, up, false, b2, b3, i)
BUSY7(S, closed, down, b1, b2, false, i) -> IDLE7(FS, closed, down, b1, b2, false, i)
BUSY7(B, closed, up, true, b2, b3, i) -> IDLE7(B, closed, stop, true, b2, b3, i)
BUSY7(FS, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, up, b1, b2, b3, i)
BUSY7(B, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, stop, b1, b2, b3, i)
start1(i) -> busy7(F, closed, stop, false, false, false, i)
busy7(BF, d, stop, b1, b2, b3, i) -> incorrect
busy7(FS, d, stop, b1, b2, b3, i) -> incorrect
busy7(fl, open, up, b1, b2, b3, i) -> incorrect
busy7(fl, open, down, b1, b2, b3, i) -> incorrect
busy7(B, closed, stop, false, false, false, empty) -> correct
busy7(F, closed, stop, false, false, false, empty) -> correct
busy7(S, closed, stop, false, false, false, empty) -> correct
busy7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(B, open, stop, false, b2, b3, i) -> idle7(B, closed, stop, false, b2, b3, i)
busy7(F, open, stop, b1, false, b3, i) -> idle7(F, closed, stop, b1, false, b3, i)
busy7(S, open, stop, b1, b2, false, i) -> idle7(S, closed, stop, b1, b2, false, i)
busy7(B, d, stop, true, b2, b3, i) -> idle7(B, open, stop, false, b2, b3, i)
busy7(F, d, stop, b1, true, b3, i) -> idle7(F, open, stop, b1, false, b3, i)
busy7(S, d, stop, b1, b2, true, i) -> idle7(S, open, stop, b1, b2, false, i)
busy7(B, closed, down, b1, b2, b3, i) -> idle7(B, closed, stop, b1, b2, b3, i)
busy7(S, closed, up, b1, b2, b3, i) -> idle7(S, closed, stop, b1, b2, b3, i)
busy7(B, closed, up, true, b2, b3, i) -> idle7(B, closed, stop, true, b2, b3, i)
busy7(F, closed, up, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(F, closed, down, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(S, closed, down, b1, b2, true, i) -> idle7(S, closed, stop, b1, b2, true, i)
busy7(B, closed, up, false, b2, b3, i) -> idle7(BF, closed, up, false, b2, b3, i)
busy7(F, closed, up, b1, false, b3, i) -> idle7(FS, closed, up, b1, false, b3, i)
busy7(F, closed, down, b1, false, b3, i) -> idle7(BF, closed, down, b1, false, b3, i)
busy7(S, closed, down, b1, b2, false, i) -> idle7(FS, closed, down, b1, b2, false, i)
busy7(BF, closed, up, b1, b2, b3, i) -> idle7(F, closed, up, b1, b2, b3, i)
busy7(BF, closed, down, b1, b2, b3, i) -> idle7(B, closed, down, b1, b2, b3, i)
busy7(FS, closed, up, b1, b2, b3, i) -> idle7(S, closed, up, b1, b2, b3, i)
busy7(FS, closed, down, b1, b2, b3, i) -> idle7(F, closed, down, b1, b2, b3, i)
busy7(B, closed, stop, false, true, b3, i) -> idle7(B, closed, up, false, true, b3, i)
busy7(B, closed, stop, false, false, true, i) -> idle7(B, closed, up, false, false, true, i)
busy7(F, closed, stop, true, false, b3, i) -> idle7(F, closed, down, true, false, b3, i)
busy7(F, closed, stop, false, false, true, i) -> idle7(F, closed, up, false, false, true, i)
busy7(S, closed, stop, b1, true, false, i) -> idle7(S, closed, down, b1, true, false, i)
busy7(S, closed, stop, true, false, false, i) -> idle7(S, closed, down, true, false, false, i)
idle7(fl, d, m, b1, b2, b3, empty) -> busy7(fl, d, m, b1, b2, b3, empty)
idle7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> busy7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
or2(true, b) -> true
or2(false, b) -> b
start1(x0)
busy7(BF, x0, stop, x1, x2, x3, x4)
busy7(FS, x0, stop, x1, x2, x3, x4)
busy7(x0, open, up, x1, x2, x3, x4)
busy7(x0, open, down, x1, x2, x3, x4)
busy7(B, closed, stop, false, false, false, empty)
busy7(F, closed, stop, false, false, false, empty)
busy7(S, closed, stop, false, false, false, empty)
busy7(B, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(F, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(S, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(B, open, stop, false, x0, x1, x2)
busy7(F, open, stop, x0, false, x1, x2)
busy7(S, open, stop, x0, x1, false, x2)
busy7(B, x0, stop, true, x1, x2, x3)
busy7(F, x0, stop, x1, true, x2, x3)
busy7(S, x0, stop, x1, x2, true, x3)
busy7(B, closed, down, x0, x1, x2, x3)
busy7(S, closed, up, x0, x1, x2, x3)
busy7(B, closed, up, true, x0, x1, x2)
busy7(F, closed, up, x0, true, x1, x2)
busy7(F, closed, down, x0, true, x1, x2)
busy7(S, closed, down, x0, x1, true, x2)
busy7(B, closed, up, false, x0, x1, x2)
busy7(F, closed, up, x0, false, x1, x2)
busy7(F, closed, down, x0, false, x1, x2)
busy7(S, closed, down, x0, x1, false, x2)
busy7(BF, closed, up, x0, x1, x2, x3)
busy7(BF, closed, down, x0, x1, x2, x3)
busy7(FS, closed, up, x0, x1, x2, x3)
busy7(FS, closed, down, x0, x1, x2, x3)
busy7(B, closed, stop, false, true, x0, x1)
busy7(B, closed, stop, false, false, true, x0)
busy7(F, closed, stop, true, false, x0, x1)
busy7(F, closed, stop, false, false, true, x0)
busy7(S, closed, stop, x0, true, false, x1)
busy7(S, closed, stop, true, false, false, x0)
idle7(x0, x1, x2, x3, x4, x5, empty)
idle7(x0, x1, x2, x3, x4, x5, newbuttons4(x6, x7, x8, x9))
or2(true, x0)
or2(false, x0)
The following pairs can be strictly oriented and are deleted.
The remaining pairs can at least by weakly be oriented.
BUSY7(F, d, stop, b1, true, b3, i) -> IDLE7(F, open, stop, b1, false, b3, i)
Used ordering: Combined order from the following AFS and order.
BUSY7(S, closed, stop, true, false, false, i) -> IDLE7(S, closed, down, true, false, false, i)
BUSY7(B, open, stop, false, b2, b3, i) -> IDLE7(B, closed, stop, false, b2, b3, i)
BUSY7(F, open, stop, b1, false, b3, i) -> IDLE7(F, closed, stop, b1, false, b3, i)
BUSY7(B, closed, stop, false, true, b3, i) -> IDLE7(B, closed, up, false, true, b3, i)
BUSY7(F, closed, stop, true, false, b3, i) -> IDLE7(F, closed, down, true, false, b3, i)
BUSY7(F, closed, stop, false, false, true, i) -> IDLE7(F, closed, up, false, false, true, i)
BUSY7(S, open, stop, b1, b2, false, i) -> IDLE7(S, closed, stop, b1, b2, false, i)
BUSY7(BF, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, down, b1, b2, b3, i)
BUSY7(BF, closed, up, b1, b2, b3, i) -> IDLE7(F, closed, up, b1, b2, b3, i)
BUSY7(B, closed, stop, false, false, true, i) -> IDLE7(B, closed, up, false, false, true, i)
BUSY7(F, closed, down, b1, false, b3, i) -> IDLE7(BF, closed, down, b1, false, b3, i)
BUSY7(FS, closed, down, b1, b2, b3, i) -> IDLE7(F, closed, down, b1, b2, b3, i)
BUSY7(S, closed, stop, b1, true, false, i) -> IDLE7(S, closed, down, b1, true, false, i)
BUSY7(S, closed, down, b1, b2, true, i) -> IDLE7(S, closed, stop, b1, b2, true, i)
BUSY7(F, closed, up, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(F, closed, up, b1, false, b3, i) -> IDLE7(FS, closed, up, b1, false, b3, i)
BUSY7(F, closed, down, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
IDLE7(fl, d, m, b1, b2, b3, empty) -> BUSY7(fl, d, m, b1, b2, b3, empty)
BUSY7(S, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, stop, b1, b2, b3, i)
BUSY7(B, closed, up, false, b2, b3, i) -> IDLE7(BF, closed, up, false, b2, b3, i)
BUSY7(S, closed, down, b1, b2, false, i) -> IDLE7(FS, closed, down, b1, b2, false, i)
BUSY7(B, closed, up, true, b2, b3, i) -> IDLE7(B, closed, stop, true, b2, b3, i)
BUSY7(FS, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, up, b1, b2, b3, i)
BUSY7(B, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, stop, b1, b2, b3, i)
stop > true > closed > down > S > open
stop > true > closed > down > B > BF > open
stop > true > closed > down > F > BF > open
stop > true > closed > FS > F > BF > open
stop > true > closed > FS > up > S > open
stop > true > closed > FS > up > BF > open
stop > true > false > down > S > open
stop > true > false > down > B > BF > open
stop > true > false > down > F > BF > open
stop > true > false > FS > F > BF > open
stop > true > false > FS > up > S > open
stop > true > false > FS > up > BF > open
empty > open
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
BUSY7(S, closed, stop, true, false, false, i) -> IDLE7(S, closed, down, true, false, false, i)
BUSY7(B, closed, stop, false, false, true, i) -> IDLE7(B, closed, up, false, false, true, i)
BUSY7(F, closed, down, b1, false, b3, i) -> IDLE7(BF, closed, down, b1, false, b3, i)
BUSY7(FS, closed, down, b1, b2, b3, i) -> IDLE7(F, closed, down, b1, b2, b3, i)
BUSY7(B, open, stop, false, b2, b3, i) -> IDLE7(B, closed, stop, false, b2, b3, i)
BUSY7(F, closed, up, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(S, closed, down, b1, b2, true, i) -> IDLE7(S, closed, stop, b1, b2, true, i)
BUSY7(S, closed, stop, b1, true, false, i) -> IDLE7(S, closed, down, b1, true, false, i)
BUSY7(F, closed, up, b1, false, b3, i) -> IDLE7(FS, closed, up, b1, false, b3, i)
BUSY7(F, open, stop, b1, false, b3, i) -> IDLE7(F, closed, stop, b1, false, b3, i)
BUSY7(B, closed, stop, false, true, b3, i) -> IDLE7(B, closed, up, false, true, b3, i)
BUSY7(F, closed, stop, true, false, b3, i) -> IDLE7(F, closed, down, true, false, b3, i)
BUSY7(F, closed, stop, false, false, true, i) -> IDLE7(F, closed, up, false, false, true, i)
BUSY7(S, open, stop, b1, b2, false, i) -> IDLE7(S, closed, stop, b1, b2, false, i)
BUSY7(BF, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, down, b1, b2, b3, i)
BUSY7(F, closed, down, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
IDLE7(fl, d, m, b1, b2, b3, empty) -> BUSY7(fl, d, m, b1, b2, b3, empty)
BUSY7(B, closed, up, false, b2, b3, i) -> IDLE7(BF, closed, up, false, b2, b3, i)
BUSY7(S, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, stop, b1, b2, b3, i)
BUSY7(BF, closed, up, b1, b2, b3, i) -> IDLE7(F, closed, up, b1, b2, b3, i)
BUSY7(S, closed, down, b1, b2, false, i) -> IDLE7(FS, closed, down, b1, b2, false, i)
BUSY7(B, closed, up, true, b2, b3, i) -> IDLE7(B, closed, stop, true, b2, b3, i)
BUSY7(B, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, stop, b1, b2, b3, i)
BUSY7(FS, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, up, b1, b2, b3, i)
start1(i) -> busy7(F, closed, stop, false, false, false, i)
busy7(BF, d, stop, b1, b2, b3, i) -> incorrect
busy7(FS, d, stop, b1, b2, b3, i) -> incorrect
busy7(fl, open, up, b1, b2, b3, i) -> incorrect
busy7(fl, open, down, b1, b2, b3, i) -> incorrect
busy7(B, closed, stop, false, false, false, empty) -> correct
busy7(F, closed, stop, false, false, false, empty) -> correct
busy7(S, closed, stop, false, false, false, empty) -> correct
busy7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(B, open, stop, false, b2, b3, i) -> idle7(B, closed, stop, false, b2, b3, i)
busy7(F, open, stop, b1, false, b3, i) -> idle7(F, closed, stop, b1, false, b3, i)
busy7(S, open, stop, b1, b2, false, i) -> idle7(S, closed, stop, b1, b2, false, i)
busy7(B, d, stop, true, b2, b3, i) -> idle7(B, open, stop, false, b2, b3, i)
busy7(F, d, stop, b1, true, b3, i) -> idle7(F, open, stop, b1, false, b3, i)
busy7(S, d, stop, b1, b2, true, i) -> idle7(S, open, stop, b1, b2, false, i)
busy7(B, closed, down, b1, b2, b3, i) -> idle7(B, closed, stop, b1, b2, b3, i)
busy7(S, closed, up, b1, b2, b3, i) -> idle7(S, closed, stop, b1, b2, b3, i)
busy7(B, closed, up, true, b2, b3, i) -> idle7(B, closed, stop, true, b2, b3, i)
busy7(F, closed, up, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(F, closed, down, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(S, closed, down, b1, b2, true, i) -> idle7(S, closed, stop, b1, b2, true, i)
busy7(B, closed, up, false, b2, b3, i) -> idle7(BF, closed, up, false, b2, b3, i)
busy7(F, closed, up, b1, false, b3, i) -> idle7(FS, closed, up, b1, false, b3, i)
busy7(F, closed, down, b1, false, b3, i) -> idle7(BF, closed, down, b1, false, b3, i)
busy7(S, closed, down, b1, b2, false, i) -> idle7(FS, closed, down, b1, b2, false, i)
busy7(BF, closed, up, b1, b2, b3, i) -> idle7(F, closed, up, b1, b2, b3, i)
busy7(BF, closed, down, b1, b2, b3, i) -> idle7(B, closed, down, b1, b2, b3, i)
busy7(FS, closed, up, b1, b2, b3, i) -> idle7(S, closed, up, b1, b2, b3, i)
busy7(FS, closed, down, b1, b2, b3, i) -> idle7(F, closed, down, b1, b2, b3, i)
busy7(B, closed, stop, false, true, b3, i) -> idle7(B, closed, up, false, true, b3, i)
busy7(B, closed, stop, false, false, true, i) -> idle7(B, closed, up, false, false, true, i)
busy7(F, closed, stop, true, false, b3, i) -> idle7(F, closed, down, true, false, b3, i)
busy7(F, closed, stop, false, false, true, i) -> idle7(F, closed, up, false, false, true, i)
busy7(S, closed, stop, b1, true, false, i) -> idle7(S, closed, down, b1, true, false, i)
busy7(S, closed, stop, true, false, false, i) -> idle7(S, closed, down, true, false, false, i)
idle7(fl, d, m, b1, b2, b3, empty) -> busy7(fl, d, m, b1, b2, b3, empty)
idle7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> busy7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
or2(true, b) -> true
or2(false, b) -> b
start1(x0)
busy7(BF, x0, stop, x1, x2, x3, x4)
busy7(FS, x0, stop, x1, x2, x3, x4)
busy7(x0, open, up, x1, x2, x3, x4)
busy7(x0, open, down, x1, x2, x3, x4)
busy7(B, closed, stop, false, false, false, empty)
busy7(F, closed, stop, false, false, false, empty)
busy7(S, closed, stop, false, false, false, empty)
busy7(B, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(F, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(S, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(B, open, stop, false, x0, x1, x2)
busy7(F, open, stop, x0, false, x1, x2)
busy7(S, open, stop, x0, x1, false, x2)
busy7(B, x0, stop, true, x1, x2, x3)
busy7(F, x0, stop, x1, true, x2, x3)
busy7(S, x0, stop, x1, x2, true, x3)
busy7(B, closed, down, x0, x1, x2, x3)
busy7(S, closed, up, x0, x1, x2, x3)
busy7(B, closed, up, true, x0, x1, x2)
busy7(F, closed, up, x0, true, x1, x2)
busy7(F, closed, down, x0, true, x1, x2)
busy7(S, closed, down, x0, x1, true, x2)
busy7(B, closed, up, false, x0, x1, x2)
busy7(F, closed, up, x0, false, x1, x2)
busy7(F, closed, down, x0, false, x1, x2)
busy7(S, closed, down, x0, x1, false, x2)
busy7(BF, closed, up, x0, x1, x2, x3)
busy7(BF, closed, down, x0, x1, x2, x3)
busy7(FS, closed, up, x0, x1, x2, x3)
busy7(FS, closed, down, x0, x1, x2, x3)
busy7(B, closed, stop, false, true, x0, x1)
busy7(B, closed, stop, false, false, true, x0)
busy7(F, closed, stop, true, false, x0, x1)
busy7(F, closed, stop, false, false, true, x0)
busy7(S, closed, stop, x0, true, false, x1)
busy7(S, closed, stop, true, false, false, x0)
idle7(x0, x1, x2, x3, x4, x5, empty)
idle7(x0, x1, x2, x3, x4, x5, newbuttons4(x6, x7, x8, x9))
or2(true, x0)
or2(false, x0)
The following pairs can be strictly oriented and are deleted.
The remaining pairs can at least by weakly be oriented.
BUSY7(B, open, stop, false, b2, b3, i) -> IDLE7(B, closed, stop, false, b2, b3, i)
BUSY7(F, open, stop, b1, false, b3, i) -> IDLE7(F, closed, stop, b1, false, b3, i)
BUSY7(S, open, stop, b1, b2, false, i) -> IDLE7(S, closed, stop, b1, b2, false, i)
Used ordering: Combined order from the following AFS and order.
BUSY7(S, closed, stop, true, false, false, i) -> IDLE7(S, closed, down, true, false, false, i)
BUSY7(B, closed, stop, false, false, true, i) -> IDLE7(B, closed, up, false, false, true, i)
BUSY7(F, closed, down, b1, false, b3, i) -> IDLE7(BF, closed, down, b1, false, b3, i)
BUSY7(FS, closed, down, b1, b2, b3, i) -> IDLE7(F, closed, down, b1, b2, b3, i)
BUSY7(F, closed, up, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(S, closed, down, b1, b2, true, i) -> IDLE7(S, closed, stop, b1, b2, true, i)
BUSY7(S, closed, stop, b1, true, false, i) -> IDLE7(S, closed, down, b1, true, false, i)
BUSY7(F, closed, up, b1, false, b3, i) -> IDLE7(FS, closed, up, b1, false, b3, i)
BUSY7(B, closed, stop, false, true, b3, i) -> IDLE7(B, closed, up, false, true, b3, i)
BUSY7(F, closed, stop, true, false, b3, i) -> IDLE7(F, closed, down, true, false, b3, i)
BUSY7(F, closed, stop, false, false, true, i) -> IDLE7(F, closed, up, false, false, true, i)
BUSY7(BF, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, down, b1, b2, b3, i)
BUSY7(F, closed, down, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
IDLE7(fl, d, m, b1, b2, b3, empty) -> BUSY7(fl, d, m, b1, b2, b3, empty)
BUSY7(B, closed, up, false, b2, b3, i) -> IDLE7(BF, closed, up, false, b2, b3, i)
BUSY7(S, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, stop, b1, b2, b3, i)
BUSY7(BF, closed, up, b1, b2, b3, i) -> IDLE7(F, closed, up, b1, b2, b3, i)
BUSY7(S, closed, down, b1, b2, false, i) -> IDLE7(FS, closed, down, b1, b2, false, i)
BUSY7(B, closed, up, true, b2, b3, i) -> IDLE7(B, closed, stop, true, b2, b3, i)
BUSY7(B, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, stop, b1, b2, b3, i)
BUSY7(FS, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, up, b1, b2, b3, i)
down > closed
up > S > closed
up > stop > closed
up > true > closed
up > false > closed
up > B > closed
up > F > closed
up > BF > closed
up > FS > closed
open > closed
empty > closed
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
BUSY7(S, closed, stop, true, false, false, i) -> IDLE7(S, closed, down, true, false, false, i)
BUSY7(B, closed, stop, false, false, true, i) -> IDLE7(B, closed, up, false, false, true, i)
BUSY7(F, closed, down, b1, false, b3, i) -> IDLE7(BF, closed, down, b1, false, b3, i)
BUSY7(FS, closed, down, b1, b2, b3, i) -> IDLE7(F, closed, down, b1, b2, b3, i)
BUSY7(F, closed, up, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
BUSY7(S, closed, down, b1, b2, true, i) -> IDLE7(S, closed, stop, b1, b2, true, i)
BUSY7(S, closed, stop, b1, true, false, i) -> IDLE7(S, closed, down, b1, true, false, i)
BUSY7(F, closed, up, b1, false, b3, i) -> IDLE7(FS, closed, up, b1, false, b3, i)
BUSY7(B, closed, stop, false, true, b3, i) -> IDLE7(B, closed, up, false, true, b3, i)
BUSY7(F, closed, stop, true, false, b3, i) -> IDLE7(F, closed, down, true, false, b3, i)
BUSY7(F, closed, stop, false, false, true, i) -> IDLE7(F, closed, up, false, false, true, i)
BUSY7(BF, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, down, b1, b2, b3, i)
BUSY7(F, closed, down, b1, true, b3, i) -> IDLE7(F, closed, stop, b1, true, b3, i)
IDLE7(fl, d, m, b1, b2, b3, empty) -> BUSY7(fl, d, m, b1, b2, b3, empty)
BUSY7(BF, closed, up, b1, b2, b3, i) -> IDLE7(F, closed, up, b1, b2, b3, i)
BUSY7(S, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, stop, b1, b2, b3, i)
BUSY7(B, closed, up, false, b2, b3, i) -> IDLE7(BF, closed, up, false, b2, b3, i)
BUSY7(S, closed, down, b1, b2, false, i) -> IDLE7(FS, closed, down, b1, b2, false, i)
BUSY7(B, closed, up, true, b2, b3, i) -> IDLE7(B, closed, stop, true, b2, b3, i)
BUSY7(FS, closed, up, b1, b2, b3, i) -> IDLE7(S, closed, up, b1, b2, b3, i)
BUSY7(B, closed, down, b1, b2, b3, i) -> IDLE7(B, closed, stop, b1, b2, b3, i)
start1(i) -> busy7(F, closed, stop, false, false, false, i)
busy7(BF, d, stop, b1, b2, b3, i) -> incorrect
busy7(FS, d, stop, b1, b2, b3, i) -> incorrect
busy7(fl, open, up, b1, b2, b3, i) -> incorrect
busy7(fl, open, down, b1, b2, b3, i) -> incorrect
busy7(B, closed, stop, false, false, false, empty) -> correct
busy7(F, closed, stop, false, false, false, empty) -> correct
busy7(S, closed, stop, false, false, false, empty) -> correct
busy7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(B, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(F, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i)) -> idle7(S, closed, stop, false, false, false, newbuttons4(i1, i2, i3, i))
busy7(B, open, stop, false, b2, b3, i) -> idle7(B, closed, stop, false, b2, b3, i)
busy7(F, open, stop, b1, false, b3, i) -> idle7(F, closed, stop, b1, false, b3, i)
busy7(S, open, stop, b1, b2, false, i) -> idle7(S, closed, stop, b1, b2, false, i)
busy7(B, d, stop, true, b2, b3, i) -> idle7(B, open, stop, false, b2, b3, i)
busy7(F, d, stop, b1, true, b3, i) -> idle7(F, open, stop, b1, false, b3, i)
busy7(S, d, stop, b1, b2, true, i) -> idle7(S, open, stop, b1, b2, false, i)
busy7(B, closed, down, b1, b2, b3, i) -> idle7(B, closed, stop, b1, b2, b3, i)
busy7(S, closed, up, b1, b2, b3, i) -> idle7(S, closed, stop, b1, b2, b3, i)
busy7(B, closed, up, true, b2, b3, i) -> idle7(B, closed, stop, true, b2, b3, i)
busy7(F, closed, up, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(F, closed, down, b1, true, b3, i) -> idle7(F, closed, stop, b1, true, b3, i)
busy7(S, closed, down, b1, b2, true, i) -> idle7(S, closed, stop, b1, b2, true, i)
busy7(B, closed, up, false, b2, b3, i) -> idle7(BF, closed, up, false, b2, b3, i)
busy7(F, closed, up, b1, false, b3, i) -> idle7(FS, closed, up, b1, false, b3, i)
busy7(F, closed, down, b1, false, b3, i) -> idle7(BF, closed, down, b1, false, b3, i)
busy7(S, closed, down, b1, b2, false, i) -> idle7(FS, closed, down, b1, b2, false, i)
busy7(BF, closed, up, b1, b2, b3, i) -> idle7(F, closed, up, b1, b2, b3, i)
busy7(BF, closed, down, b1, b2, b3, i) -> idle7(B, closed, down, b1, b2, b3, i)
busy7(FS, closed, up, b1, b2, b3, i) -> idle7(S, closed, up, b1, b2, b3, i)
busy7(FS, closed, down, b1, b2, b3, i) -> idle7(F, closed, down, b1, b2, b3, i)
busy7(B, closed, stop, false, true, b3, i) -> idle7(B, closed, up, false, true, b3, i)
busy7(B, closed, stop, false, false, true, i) -> idle7(B, closed, up, false, false, true, i)
busy7(F, closed, stop, true, false, b3, i) -> idle7(F, closed, down, true, false, b3, i)
busy7(F, closed, stop, false, false, true, i) -> idle7(F, closed, up, false, false, true, i)
busy7(S, closed, stop, b1, true, false, i) -> idle7(S, closed, down, b1, true, false, i)
busy7(S, closed, stop, true, false, false, i) -> idle7(S, closed, down, true, false, false, i)
idle7(fl, d, m, b1, b2, b3, empty) -> busy7(fl, d, m, b1, b2, b3, empty)
idle7(fl, d, m, b1, b2, b3, newbuttons4(i1, i2, i3, i)) -> busy7(fl, d, m, or2(b1, i1), or2(b2, i2), or2(b3, i3), i)
or2(true, b) -> true
or2(false, b) -> b
start1(x0)
busy7(BF, x0, stop, x1, x2, x3, x4)
busy7(FS, x0, stop, x1, x2, x3, x4)
busy7(x0, open, up, x1, x2, x3, x4)
busy7(x0, open, down, x1, x2, x3, x4)
busy7(B, closed, stop, false, false, false, empty)
busy7(F, closed, stop, false, false, false, empty)
busy7(S, closed, stop, false, false, false, empty)
busy7(B, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(F, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(S, closed, stop, false, false, false, newbuttons4(x0, x1, x2, x3))
busy7(B, open, stop, false, x0, x1, x2)
busy7(F, open, stop, x0, false, x1, x2)
busy7(S, open, stop, x0, x1, false, x2)
busy7(B, x0, stop, true, x1, x2, x3)
busy7(F, x0, stop, x1, true, x2, x3)
busy7(S, x0, stop, x1, x2, true, x3)
busy7(B, closed, down, x0, x1, x2, x3)
busy7(S, closed, up, x0, x1, x2, x3)
busy7(B, closed, up, true, x0, x1, x2)
busy7(F, closed, up, x0, true, x1, x2)
busy7(F, closed, down, x0, true, x1, x2)
busy7(S, closed, down, x0, x1, true, x2)
busy7(B, closed, up, false, x0, x1, x2)
busy7(F, closed, up, x0, false, x1, x2)
busy7(F, closed, down, x0, false, x1, x2)
busy7(S, closed, down, x0, x1, false, x2)
busy7(BF, closed, up, x0, x1, x2, x3)
busy7(BF, closed, down, x0, x1, x2, x3)
busy7(FS, closed, up, x0, x1, x2, x3)
busy7(FS, closed, down, x0, x1, x2, x3)
busy7(B, closed, stop, false, true, x0, x1)
busy7(B, closed, stop, false, false, true, x0)
busy7(F, closed, stop, true, false, x0, x1)
busy7(F, closed, stop, false, false, true, x0)
busy7(S, closed, stop, x0, true, false, x1)
busy7(S, closed, stop, true, false, false, x0)
idle7(x0, x1, x2, x3, x4, x5, empty)
idle7(x0, x1, x2, x3, x4, x5, newbuttons4(x6, x7, x8, x9))
or2(true, x0)
or2(false, x0)